ABSTRACT. Symbolic execution is a classical program analysis technique used to show that programs satisfy or violate given specifications. In this work we generalize symbolic execution to support program analysis for relational specifications in the form of relational properties - these are properties about two runs of two programs on related inputs, or about two executions of a single program on related inputs. Relational properties are useful to formalize notions in security and privacy, and to reason about program optimizations. We design a relational symbolic execution engine, named RelSym which supports interactive refutation, as well as proving of relational properties for programs written in a language with arrays and for-like loops.

ABSTRACT. Compositional compiler verification aims to ensure correct compilation of components, not just whole programs. Perconti and Ahmed (ESOP 2014) proposed a methodology for compositional compiler correctness that supports linking with code of arbitrary provenance (e.g., compiled from a different source language). To date, theirs is the only result that has been shown to allow compiled components to be linked with code whose functionality cannot even be expressed in the compiler's own source language. The essence of their approach is to define a multi-language system that formalizes interoperability between the source and target languages so that compiler correctness can be stated as contextual equivalence in the multi-language. They illustrate this methodology on a two-pass type-preserving compiler for a polymorphic language with recursive types.

In this paper, we show how to extend this multi-language compiler-verification approach to a source language with ML-style mutable references. We present the first compositional correctness proof of typed closure conversion for a language with mutable state. More importantly, we show we can extend our target language with first-class control (call/cc) yielding a compiler correctness theorem that allows components compiled from the source language (without call/cc) to be linked with target-language components (with call/cc) whose extensional behavior cannot be expressed in the source. A nontrivial technical contribution of our work is the design of the multi-language logical relation used to carry out the proof of compiler correctness. This is semantically challenging due to the mix of parametric polymorphism and mutable state in both of the interoperating languages.

ABSTRACT. Software that models how people work is omnipresent in today's society. Current languages and frameworks often focus on usability by non-programmers, sacrificing flexibility and high level abstraction. Task-oriented programming (TOP) is a programming paradigm that aims to provide the desired level of abstraction while still being expressive enough to describe real world collaboration. It prescribes a declarative programming style to specify multi-user workflows. Workflows can be higher-order. They communicate through typed values on a local and global level. Such specifications can be turned into interactive applications for different platforms, supporting collaboration during execution. TOP has been around for more than a decade, in the forms of iTasks and mTasks, which are tailored for real-world usability. So far, it has not been given a formalisation which is suitable for formal reasoning.

In this paper we give a description of the TOP paradigm and then decompose its rich features into elementary language elements, which makes them suitable for formal treatment. We use the simply typed lambda-calculus, extended with pairs and references, as a base language. On top of this language, we develop TopHat, a language for modular interactive workflows. We describe TopHat by means of a layered semantics. These layers consist of multiple big-step evaluations on expressions, and two labelled transition systems, handling user inputs.

With TopHat we prepare a way to formally reason about TOP languages and programs. This approach allows for comparison with other work in the field. We have implemented the semantic rules of TopHat in Haskell, and the task layer on top of the iTasks framework. This shows that our approach is feasible, and lets us demonstrate the concepts by means of illustrative case studies. TOP has been applied in projects with the Dutch coast guard, tax office, and navy. Our work matters because formal program verification is important for mission-critical software, especially for systems with concurrency.

ABSTRACT. FRP is an approach to declarative programming of reactive systems by describing interactions between time-varying values. FRP implementations are often realised as an embedding in a functional host language, making for very expressive reactive programming frameworks. However, this expressiveness comes at a cost: current embedded FRP implementations incur substantial performance overheads, in particular for values that (notionally) vary continuously. The basic idea of FRP is closely related to synchronous data-flow and continuous-system simulation languages. In contrast to FRP, these handle values that vary continuously efficiently, but are less expressive. This paper seeks to bridge this gap by proposing a novel approach to embedded FRP-implementation that uses the fundamental implementation approach of synchronous dataflow and simulation languages for efficient handling of continuously varying values, while retaining the expressiveness normally associated with FRP, as well as paying attention to values that only change relatively infrequently. These ideas are applicable beyond FRP, for example for implementing flexible embedded simulation languages. We evaluate our approach on a range of benchmarks, including an existing full-fledged video game where using our new FRP implementation as a drop-in replacement for the old one gave a three-fold performance improvement.

ABSTRACT. We present the design of a new functional programming language, MLTS, that uses the lambda-tree syntax approach to encoding bindings appearing within data structures. In this setting, bindings never become free nor escape their scope: instead, binders in data structures are permitted to move into binders within programs. The design of MLTS---whose concrete syntax is based on that of OCaml---includes additional sites within programs that directly support this movement of bindings. We illustrate the features of MLTS by presenting several collections of examples. We also present a typing discipline that naturally extends the typing of OCaml programs. In order to formally define the language's operational semantics, we present an abstract syntax for MLTS and a natural semantics for its evaluation. We shall view such natural semantics as a logical theory with a rich logic that includes both nominal abstraction and the nabla-quantifier: as a result, the natural semantic specification of MLTS can be given a succinct and elegant presentation. A small step semantics and a typing system are also presented.

ABSTRACT. Search strategies are crucial to efficiently solve constraint satisfaction problems. However, programming search strategies in the existing constraint solvers is a daunting task and constraint-based languages usually have compositionality issues. We propose spacetime programming, a paradigm extending the synchronous language \textsf{Esterel} and \textit{timed concurrent constraint programming} with backtracking, for creating and composing search strategies. In this formalism, the search strategies are composed in the same way as we compose concurrent processes. Our contributions include the design and behavioral semantics of spacetime programming, and the proofs that spacetime programs are deterministic, reactive and extensive functions. Moreover, spacetime programming provides a bridge between theoretical foundation of constraint-based concurrency and the practical aspects of constraint solving. We developed a prototype of the compiler that produces search strategies with a small overhead compared to the hard-coded ones.