Programming Languages
We consider the verification of lock-free data structures that manually manage their memory with the help of a safe memory reclamation (SMR) algorithm. Our first contribution is a type system that checks whether a program properly manages…
Adding versatile interactions to imperative programming -- C, Java and Android -- is an essential task. Unfortunately, existing languages provide only limited constructs for user interaction. These constructs are usually in the form of…
Programming digital contracts comes with unique challenges, which include (i) expressing and enforcing protocols of interaction, (ii) controlling resource usage, and (iii) preventing the duplication or deletion of a contract's assets. This…
While visualizations play a crucial role in gaining insights from data, generating useful visualizations from a complex dataset is far from an easy task. Besides understanding the functionality provided by existing visualization libraries,…
This volume constitutes the pre-proceedings of the DECLARE 2019 conference, held on September 9 to 13, 2019 at the University of Technology Cottbus - Senftenberg (Germany). Declarative programming is an advanced paradigm for the modeling…
We propose the first framework for defining relational program logics for arbitrary monadic effects. The framework is embedded within a relational dependent type theory and is highly expressive. At the semantic level, we provide an…
Automatic generation of software from some form of specification has been a long standing goal of computer science research. To date successful results have been reported for the production of relatively small programs. This paper presents…
Blockchains are becoming increasingly relevant in a variety of fields, such as finance, logistics, and real estate. The fundamental task of a blockchain system is to establish data consistency among distributed agents in an open network.…
Session types are a rich type discipline, based on linear types, that lifts the sort of safety claims that come with type systems to communications. However, web-based applications and microservices are often written in a mix of languages,…
Probabilistic programming is the idea of writing models from statistics and machine learning using program notations and reasoning about these models using generic inference engines. Recently its combination with deep learning has been…
In this work, we study 'reduction monads', which are essentially the same as monads relative to the free functor from sets into multigraphs. Reduction monads account for two aspects of the lambda calculus: on the one hand, in the monadic…
"Interaction trees" (ITrees) are a general-purpose data structure for representing the behaviors of recursive programs that interact with their environments. A coinductive variant of "free monads," ITrees are built out of uninterpreted…
In recent years, languages like Haskell have seen a dramatic surge of new features that significantly extends the expressive power of their type systems. With these features, the challenge of kind inference for datatype declarations has…
An oblivious computation is one that is free of direct and indirect information leaks, e.g., due to observable differences in timing and memory access patterns. This paper presents Lambda Obliv, a core language whose type system enforces…
Pattern matching is an important feature of programming languages for data abstraction. Many pattern-matching extensions have been proposed and implemented for extending the range of data types to which pattern matching is applicable. Among…
The main way of analyzing the complexity of a program is that of extracting and solving a recurrence that expresses its running time in terms of the size of its input. We develop a method that automatically extracts such recurrences from…
Information-flow security type systems ensure confidentiality by enforcing noninterference: a program cannot leak private data to public channels. However, in practice, programs need to selectively declassify information about private data.…
This paper presents Gemini, a functional programming language for hardware description that provides features such as parametric polymorphism, recursive datatypes, higher-order functions, and type inference for higher expressivity compared…
This paper presents a method for synthesizing a reactive program which coordinates the actions of a group of other reactive programs, so that the combined system satisfies a temporal specification of its desired long-term behavior.…
Session types have emerged as a typing discipline for communication protocols. Existing calculi with session types come equipped with many different primitives that combine communication with the introduction or elimination of the…