Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top

2021 | Book

A Family of Unification-Oblivious Program Transformations and Their Applications Read chapter Read first chapter

Practical Aspects of Declarative Languages

23rd International Symposium, PADL 2021, Copenhagen, Denmark, January 18-19, 2021, Proceedings

Editors: Dr. José F. Morales, Dominic Orchard

Publisher: Springer International Publishing

Book Series : Lecture Notes in Computer Science

Part of: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Login to get access
insite
SEARCH

About this book

This book constitutes the refereed proceedings of the 23rd International Symposium on Practical Aspects of Declarative Languages, PADL 2021, held in Copenhagen, Denmark, in January 2021.

The 10 full papers were carefully reviewed and selected from 21 submissions. The papers present original work emphasizing novel applications and implementation techniques for all forms of declarative concepts, including programming with sets, functions, logic, and constraints. The papers are organized in the following topical headings:

Foundations and Programming Concepts; Applications of Declarative Languages, and Declarative Approaches to Testing and Debugging.

Due to the Corona pandemic PADL 2021 was held as a virtual event.

Table of Contents

Frontmatter

Foundations and Programming Concepts

Frontmatter
A Family of Unification-Oblivious Program Transformations and Their Applications
Abstract
We describe a family of program transformations that compile a Horn Clause program into equivalent programs of a simpler and more regular structure.
Our transformations, seen as morphisms between term algebras, commute with unification, clause unfoldings and Prolog’s LD-resolution, thus preserving the operational semantics of the Horn Clause programs.
As applications, the resulting programs have simpler execution algorithms and can be compiled to minimalist instruction sets.
Paul Tarau
On Adding Pattern Matching to Haskell-Based Deeply Embedded Domain Specific Languages
Abstract
Capturing control flow is the Achilles heel of Haskell-based deeply embedded domain specific languages. Rather than use the builtin control flow mechanisms, artificial control flow combinators are used instead. However, capturing traditional control flow in a deeply embedded domain specific language would support the writing of programs in a natural style by allowing the programmer to use the constructs that are already builtin to the base language, such as pattern matching and recursion. In this paper, we expand the capabilities of Haskell-based deep embeddings with a compiler extension for reifying conditionals and pattern matching. With this new support, the subset of Haskell that we use for expressing deeply embedded domain specific languages can be cleaner, Haskell-idiomatic, and more declarative in nature.
David Young, Mark Grebe, Andy Gill
Synchronous Message-Passing with Priority
Abstract
In this paper we introduce a tiered-priority mechanism for a synchronous message-passing language with support for selective communication and first-class communication protocols. Crucially our mechanism allows higher priority threads to communicate with lower priority threads, providing the ability to express programs that would be rejected by classic priority mechanisms that disallow any (potentially) blocking interactions between threads of differing priorities. We provide a prototype implementation of our tiered-priority mechanism capable of expressing Concurrent ML and built in the MLton SML compiler and runtime. We evaluate the viability of our implementation by implementing a safe and predictable shutdown mechanisms in the Swerve webserver and eXene windowing toolkit. Our experiments show that priority can be easily added to existing CML programs without degrading performance. Our system exhibits negligible overheads on more modest workloads.
Cheng-En Chuang, Grant Iraci, Lukasz Ziarek

Open Access

Putting Gradual Types to Work
Abstract
In this paper, we describe our experience incorporating gradual types in a statically typed functional language with Hindley-Milner style type inference. Where most gradually typed systems aim to improve static checking in a dynamically typed language, we approach it from the opposite perspective and promote dynamic checking in a statically typed language. Our approach provides a glimpse into how languages like SML and OCaml might handle gradual typing. We discuss our implementation and challenges faced—specifically how gradual typing rules apply to our representation of composite and recursive types. We review the various implementations that add dynamic typing to a statically typed language in order to highlight the different ways of mixing static and dynamic typing and examine possible inspirations while maintaining the gradual nature of our type system. This paper also discusses our motivation for adding gradual types to our language, and the practical benefits of doing so in our industrial setting.
Bhargav Shivkumar, Enrique Naudon, Lukasz Ziarek
PDF View full text

Applications of Declarative Languages

Frontmatter
A Logic Programming Approach to Regression Based Repair of Incorrect Initial Belief States
Abstract
This paper explores the challenge of encountering incorrect beliefs in the context of reasoning about actions and changes using action languages with sensing actions. An incorrect belief occurs when some observations conflict with the agent’s own beliefs. A common approach to recover from this situation is to replace the initial beliefs with beliefs that conform to the sequence of actions and the observations. The paper introduces a regression-based and revision-based approach to calculate a correct initial belief. Starting from an inconsistent history consisting of actions and observations, the proposed framework (1) computes the initial belief states that support the actions and observations and (2) uses a belief revision operator to repair the false initial belief state. The framework operates on domains with static causal laws, supports arbitrary sequences of actions, and integrates belief revision methods to select a meaningful initial belief state among possible alternatives.
Fabio Tardivo, Loc Pham, Tran Cao Son, Enrico Pontelli
Data Validation Meets Answer Set Programming
Abstract
Data validation may save the day of computer programmers, whatever programming language they use. In fact, processing invalid data is a waste of resources at best, and a drama at worst if the problem remains unnoticed and wrong results are used for business. Answer Set Programming is not an exception, but the quest for better and better performance resulted in systems that essentially do not validate data in any way. Even under the simplistic assumption that input and output data are eventually validated by external tools, invalid data may appear in other portions of the program, and go undetected until some other module of the designed software suddenly breaks. This paper formalizes the problem of data validation for ASP programs, introduces a declarative language to specify data validation, and presents a tool to inject data validation in ordinary programs. The proposed approach promotes fail-fast techniques at coding time without imposing any lag on the deployed system if data are pretended to be valid. Additionally, the proposed approach opens the possibility to take advantage of ASP declarativity for validating complex data of imperative programming languages.
Mario Alviano, Carmine Dodaro, Arnel Zamayla
Lightweight Declarative Server-Side Web Programming
Abstract
Web interfaces are an important part of many applications but their implementation is full of pitfalls due to the client/server nature of web programming. This paper presents a lightweight approach to web programming based on a standard infrastructure, in particular, the common CGI protocol between client and server. No specific additions are necessary on the server side. Our approach exploits declarative programming features to provide a high-level API for server-side web scripting. This API allows to check many programming errors at compile time by using functional (static typing, higher-order functions) as well as logic (free variables) programming features. Together with further abstractions, like session handling, persistence, and typeful database access, it is used for non-trivial web applications.
Michael Hanus

Declarative Approaches to Testing and Debugging

Frontmatter

Open Access

ConFuzz: Coverage-Guided Property Fuzzing for Event-Driven Programs
Abstract
Bug-free concurrent programs are hard to write due to non-determinism arising out of concurrency and program inputs. Since concurrency bugs typically manifest under specific inputs and thread schedules, conventional testing methodologies for concurrent programs like stress testing and random testing, which explore random schedules, have a strong chance of missing buggy schedules.
In this paper, we introduce a novel technique that combines property-based testing with mutation-based, grey box fuzzer, applied to event-driven OCaml programs. We have implemented this technique in ConFuzz, a directed concurrency bug-finding tool for event-driven OCaml programs. Using ConFuzz, programmers specify high-level program properties as assertions in the concurrent program. ConFuzz uses the popular greybox fuzzer AFL to generate inputs as well as concurrent schedules to maximise the likelihood of finding new schedules and paths in the program so as to make the assertion fail. ConFuzz does not require any modification to the concurrent program, which is free to perform arbitrary I/O operations. Our experimental results show that ConFuzz is easy-to-use, effective, detects concurrency bugs faster than Node.Fz - a random fuzzer for event-driven JavaScript programs, and is able to reproduce known concurrency bugs in widely used OCaml libraries.
Sumit Padhiyar, K. C. Sivaramakrishnan
PDF View full text
Causal-Consistent Reversible Debugging: Improving CauDEr
Abstract
Causal-consistent reversible debugging allows one to explore concurrent computations back and forth in order to locate the source of an error. In this setting, backward steps can be chosen freely as long as they are causal consistent, i.e., as long as all the actions that depend on the action we want to undo have been already undone. Here, we consider a framework for causal-consistent reversible debugging in the functional and concurrent language Erlang. This framework considered programs translated to an intermediate representation, called Core Erlang. Although using such an intermediate representation simplified both the formal definitions and their implementation in a debugging tool, the choice of Core Erlang also complicated the use of the debugger. In this paper, we extend the framework in order to deal with source Erlang programs, also including some features that were not considered before. Moreover, we integrate the two existing approaches (user-driven debugging and replay debugging) into a single, more general framework, and develop a new version of the debugging tool CauDEr including all the mentioned extensions as well as a renovated user interface.
Juan José González-Abril, Germán Vidal
Declarative Debugging of XML Queries
Abstract
In this paper we present the elements of an algorithmic debugger for XQuery. Given a XQuery program/query, a debugging tree is built in which the root is the query and the answer, and non-root nodes contain the results of function calls and XPath expressions computed from the query. Using the higher-order capabilities of XQuery several navigation strategies can be defined, enabling the adaptation of the debugging to the program/query and the user needs. Debugging trees and concepts as (partially) incomplete and incorrect answers are formally defined for queries in terms of XQuery semantics. A Web tool has been developed allowing the visualization of the debugging tree and the debugging of a XQuery program/query with the selected navigation strategy.
Jesús M. Almendros-Jiménez, Antonio Becerra-Terón
Backmatter
Metadata
Title
Practical Aspects of Declarative Languages
Editors
Dr. José F. Morales
Dominic Orchard
Copyright Year
2021
Electronic ISBN
978-3-030-67438-0
Print ISBN
978-3-030-67437-3
DOI
https://doi.org/10.1007/978-3-030-67438-0

Premium Partner

    Image Credits