PLNL 2018: First VERSEN Workshop on Programming Languages in The Netherlands

With the proliferation of blockchain designs, we see a proliferation of proposals for languages and systems to script the rules governing transactions on these blockchains, generally known as smart contract languages. Despite the name, these languages are usually fairly conventional programming languages used to impose constraints on the transactions permitted to transfer assets and manipulate data on the blockchain.

Given the high financial stakes and widely publicised exploits on first and second generation blockchains, the third-generation Cardano blockchain includes a new approach to contract languages based on state-of-the art research in programming languages and the increased safety provided by functional programming. The benefits of functional programming go even further: they provide increased flexibility in choosing a blockchain architecture and help to seamlessly combine on-chain and off-chain computations.

In this talk, I will outline how programming language research, functional programming, and Haskell help us designing and implementing a next-generation blockchain contract platform. I am also going to highlight interesting open problems and opportunities for further research. This is still a young field, and it needs more research to establish the foundations.

Manuel Chakravarty

Tweag I/O & IOHK

Netherlands

First-order theorem provers based on superposition, such as E, SPASS, and Vampire, play an important role in formal software verification. They are based on sophisticated logical calculi that combine ordered resolution and equality reasoning. They also employ advanced algorithms, data structures, and heuristics.

As a step towards verifying the correctness of state-of-the-art provers, we specify, using the Isabelle/HOL proof assistant, a purely functional ordered resolution prover and formally establish its soundness and refutational completeness. Methodologically, we apply stepwise refinement to obtain, from an abstract specification of a nondeterministic prover, a verified deterministic program, written in a subset of Isabelle/HOL from which we extract purely functional Standard ML code that constitutes a semidecision procedure for first-order logic.

(See http://matryoshka.gforge.inria.fr/pubs/fun_rp_paper.pdf for details.)

Anders Schlichtkrull

Technical University of Denmark

Jasmin Blanchette

Vrije Universiteit Amsterdam

Netherlands

Dmitriy Traytel

ETH Zurich

Switzerland

Dependent type theory allows us to write programs and to prove properties about those programs in the same language. However, some properties do not require much proof, as they are evident from a program’s implementation, e.g. if a polymorphic program is not ad hoc but relationally parametric, then we get parametricity theorems for free. If we want to safely shortcut proofs by relying on the evident good behaviour of a program, then we need a type-level guarantee that the program is indeed well-behaved. This can be achieved by annotating function types with a modality describing the behaviour of functions.

We consider a dependent type system with modalities for relational parametricity, irrelevance (i.e. type-checking time erasability of an argument) and ad hoc polymorphism. The interplay of three modalities and dependent types raises a number of questions. For example: If a term depends on a variable with a given modality, then how should its type depend on it? Are all modalities always applicable, e.g. should we consider parametric functions from the booleans to the naturals? Do we need any further modalities in order to properly reason about these three?

We develop a type system, based on a denotational presheaf model, that answers these questions. The core idea is to equip every type with a number of relations — just equality for small types, but more for larger types — and to describe function behaviour by saying how functions act on those relations. The system has modality-aware equality judgements (ignoring irrelevant parts) and modality-aware proving operators (for proving free theorems) which are even self-applicable. It also supports sized types, some form of intersection and union types, and parametric quantification over algebraic structures. We prove soundness in a denotational presheaf model.

Andreas Nuyts

KU Leuven, Belgium

Belgium

Dominique Devriese

Vrije Universiteit Brussel, Belgium

Belgium

As Rascal (https://www.rascal-mpl.org) is being applied to larger and larger problems in software analysis, software transformation and the construction of industrial domain-specific languages in domains as diverse as finance, forensics, privacy and gaming, the need for more and more speed becomes apparent.

In this presentation I will describe two consecutive efforts in building a Rascal to JVM byte code compiler. The first effort is based on a hand-written type checker and uses coroutines as execution mechanism for Rascal’s pattern matching. Although this compiler leads to faster execution and is being used we will analyze why it disappoints.

The second effort is work in progress and amounts to creating and applying TypePal (a new constraint-based type checking framework) for type checking and to replacing coroutines by a variant of continuations that can be efficiently mapped to the JVM. We expect that this second effort will bring Rascal’s performance close to that of Java.

Paul Klint

These days, parallel computing hardware is ubiquitous. However, parallel programs are typically much more difficult to write than sequential ones, so making use of all of the parallelism available in a modern computer remains difficult. Functional programming languages offer a radical and elegant attack on this challenge, by tackling the root cause of the problem, namely, unrestricted side effects.

In this talk I will reflect on the progress and challenges we have had in developing the programming language Accelerate, an embedded language in Haskell for data-parallel array programming, which exposes only a collection-oriented interface over immutable arrays. I will discuss some of the aspects to making such a language design practicable and performant, and give some examples of how this more restrictive programming model can help guide the programmer towards an efficient parallel implementations of their algorithm.

Trevor L. McDonell

Utrecht University

Netherlands

One of the cornerstones of functional programming languages is pattern matching. However, many students struggle with the concept, and end up using constructs such as isNothing or fromJust. I will present the sketch of a system I am developing which can convert automatically from bad style into a series of pattern matches.

Alejandro Serrano

Utrecht University, Netherlands

Netherlands

Definitional interpreters are an approach to specifying the semantics of an object language by implementing an interpreter in a meta language. The approach is attractive because it supports clear and concise specifications that are validatable-by-construction through execution. If we use a dependently typed meta language we seemingly get even more benefits: we can write intrinsically typed interpreters that are safe-by-construction, thereby alleviating the need for tedious and manual type soundness proofs. But implementing intrinsically typed interpreters is challenging. Data structures must be engineered to allow dependently typed host languages to infer their safe usage. And language extensions may require subtle and far reaching modifications. Furthermore, since intrinsically typed interpreters operate on intrinsically typed syntax, specification validatability is dependent on either manually constructing a well-typedness proof for each input program, or on writing a type checker that does it for us. This talk will summarize recent advances towards scaling intrinsically typed interpreters to object languages with imperative features, and discuss open problems with supporting language evolution and scaling the approach to even more object languages.

Casper Bach Poulsen

Delft University of Technology

Effect handling is a way to structure and scope side-effects which is gaining popularity as an alternative to monads in purely functional programming languages. Languages with support for effect handling allow the programmer to define idioms for state, exception handling, asynchrony, backtracking etc. from within the language. Functional programming languages, however, operate within a closed world assumption, which prohibits certain patterns of polymorphism well-known from object-oriented languages. In this paper we introduce JEff, an object-oriented programming language with native support for effect handling, to provide first answers to the question what it would mean to integrate OO programming with effect handling. We illustrate how user defined effects could benefit from interface polymorphism, and present its runtime semantics and type system.

Pablo Inostroza

CWI

Netherlands

Tijs van der Storm

Centrum Wiskunde & Informatica / University of Groningen

Netherlands

In a language with a reversible semantics, computation steps can be undone: a program can perform standard forward steps, but also backward steps. Reversibility is at the heart of mechanisms in program debugging, error recovery, and compensation handling in transactions.

Reversing a sequential program is easy: it suffices to have a memory that records information about forward steps in case we wish to return to a prior state using a backward step. Reversing a concurrent program is much more difficult: since control may simultaneously reside in more than one point, memories should record information about the steps performed in each thread, but also about the causal dependencies between steps from different threads.

The subtleties of reversibility in a concurrent setting motivate the definition of reversible semantics which are causally consistent, i.e., that ensure that backward steps lead to states that could been have reached by performing forward steps only. A causally consistent semantics never leads to states that are not reachable through forward steps.

This talk will discuss the challenges of reversible concurrency from theoretical and practical standpoints. It will be based on two recent papers (PPDP’17 and TFP’18).

On the theoretical side (PPDP’17), we will present a process model of multiparty protocols with reversibility. This formal model relies on pi-calculus processes that exchange (higher-order) messages following choreographies, as defined by multiparty session types that specify intended protocol executions. The model is equipped with a reversible operational semantics which is causally consistent.

On the practical side (TFP’18), we have developed a Haskell implementation of the reversible operational semantics in the PPDP’17 paper. We exploit algebraic data types to faithfully represent three core ingredients: a process calculus, multiparty session types, and forward/backward reduction semantics. Our implementation bears witness to the convenience of pure functional programming for implementing reversible languages.

Folkert de Vries

University of Groningen

Jorge A. Pérez

University of Groningen, The Netherlands

Netherlands

Abstract interpretation is a methodology for defining sound static analyses. Yet, creating a new static analyzer is a laborious and difficult task, because the analyzer is often implemented from scratch and proven sound a posteriori. To address this problem, we propose a novel approach to construct abstract interpreters from reusable analyses components. Each analysis component captures a separate aspect of the analyzed language (stores, environments, exceptions, etc.). Furthermore, analysis components can be proven sound a priori and their soundness proof remains valid when composing components. We developed a framework for reusable analysis components in Haskell for arrow-based abstract interpreters and realized 10 sound and reusable analysis components. We (re)used these components to define a $k$-CFA analysis for PCF and a reaching definition analysis for a While language.

Sven Keidel

Delft University of Technology, Netherlands

Netherlands

Sebastian Erdweg

Delft University of Technology, Netherlands

Netherlands

Task Oriented Programming (TOP) is a novel programming paradigm originally created to implement collaborative reactive multi-user systems. A task in TOP is a description of what needs to be done. Each task is specified by a function and evaluated at an event. The result of this evaluation is observable by other tasks even if the task is not finished. A program is a composition of tasks. The iTasks system is an implementation of TOP based on web-servers. For example, it is very suitable to program Microcontroller Units (MCUs) because they often follow similar design patterns. To cope with to the memory and processing limitations of MCUs we defined the embedded Domain Specific Language (eDSL) mTask. In this presentation, we introduce mTask and show how it is implemented such that tasks can be dynamically shipped to an MCU and executed there. MTask tasks can be generated by iTasks programs. They can communicate via Shared Data Sources (SDSs). With this new technique, one can make an entire Internet of Things (IoT) system in a single statically typed source program. This prevents many maintenance and version problems rooting from the impedance mismatch.

Mart Lubbers

Radboud University Nijmegen

Pieter Koopman

Radboud University Nijmegen, Netherlands

Netherlands

Rinus Plasmeijer

Radboud University Nijmegen

Types in programming languages serve to rule out nonsensical programs. Although untyped languages provide flexibility, they can contain subtle bugs. Types can be intrinsic or extrinsic depending on whether they appear annotated in the source program or not. For intrinsic types, the compiler verifies that a program admits a given type (type checking); for extrinsic types the compiler infers an appropriate type (type inference). Type annotations can be cumbersome in a practice, and so extrinsic types are desirable.

There are trade-offs between expressiveness and static guarantees. System F is an expressive type system that exhibits parametric polymorphism, which can enable code reuse in practice. Unfortunately, type inference is undecidable for System F. Robin Milner invented the ML language as a restricted variant of System F with a decidable type inference.

In this talk, I will discuss how we adapted results of constraint-based type systems to develop a modular ML type inference algorithm in Haskell. We use constraints as an intermediate representation, which enables a modular type inference algorithm.

The idea of a modularity is that a compiler only produces constraints and invokes an independent solver. The strengths are extensibility, complexity reasoning, and easier proofs of properties. HM(X) is a constraint-based generalization of Damas-Milner type system parametrized by constraints. For ML, we use syntactic equality constraints. Our representation consists of generation, transformation, and constraint solving. We present the generation and transformation functions suitable for a Haskell implementation. In the constraint generation stage, a ML program is translated to constraints. The constraint transformation stage translates constraints to a form solvable by first-order unification. We consider an important optimization step: avoiding multiple solving of a same constraint set that can be caused by let expression. In the constraint solving stage, the Robinson’s algorithm for first-order unification is implemented.

Alen Arslanagić

University of Groningen