Functional BIP: Embedding connectors in functional programming languages

This paper presents a theoretical foundation for functional language implementations of Behaviour–Interaction–Priority (BIP). We introduce a set of connector combinators describing synchronisation, data transfer, priorities and dynamicity in a principled way. A static type system ensures the soundness of connector semantics. Based on this foundation, we implemented BIP as an embedded domain specific language (DSL) in Haskell and Scala. The DSL embedding allows programmers to benefit from the full expressive power of high-level languages. The clear separation of behaviour and coordination inherited from BIP leads to systems that are arguably simpler to maintain and reason about, compared to other approaches.

Verified Functional Programming

Nicolas Charles Yves Voirol

In this thesis, we present Stainless, a verification system for an expressive subset of the Scala language. Our system is based on a dependently-typed language and an algorithmic type checking procedure which ensures total correctness. We rely on SMT solvers to automate the verification process and to provide us with useful counterexamples when considered properties are invalid. We then enable verification in the presence of high-level Scala language features by encoding them into the dependently-typed language. We introduce an SMT-backed counterexample finding procedure which can also prove that no counterexample exists. The procedure incrementally unfolds function calls and applications in order to progressively explore the space of counterexamples. We present increasingly expressive fragments of our dependently-typed language and establish soundness and completeness properties of the procedure for each fragment. We then describe an extension which introduces support for quantifier reasoning. We discuss syntactic and semantic conditions under which the extended procedure can produce valid counterexamples in the presence of universal quantification. We present a bidirectional type checking algorithm for our dependent type system. The algorithm relies on our counterexample finding procedure to discharge verification conditions which enables predictable and effective type checking. The type system features a unified treatment of both recursive and corecursive definitions, and further admits mutual recursion between type and function definitions. We establish normalization through a sized types approach. We define a logical relation which associates a set of reducible values to each type, and then show soundness of verification by proving that evaluation of a type checked expression terminates with a reducible value. We further discuss a set of transformations which encode high-level Scala constructs into our dependently-typed language. These transformations allow our verification system to support object-oriented features such as traits and classes with multiple inheritance, as well as abstract and concrete methods with overriding. We further present a measure inference transformation which enables automated termination checking in our system. In addition to encoding language features, we discuss how Scala can be augmented with natural specification constructs and annotations that empower verification. Finally, we describe the system implementation and discuss certain practical considerations. We show that the resulting system is effective by evaluating it on a set of benchmarks and case studies comprising over 15K lines of Scala code. These benchmarks showcase both the breadth and flexibility of the system.

EPFL2019

Type-Safe Metaprogramming and Compilation Techniques For Designing Efficient Systems in High-Level Languages

Lionel Emile Vincent Parreaux

Software engineering practices have been steadily moving towards higher-level programming languages and away from lower-level ones. High-level languages tend to greatly improve safety, productivity, and code maintainability because they handle various implementation details automatically, allowing programmers to focus on their problem domains. However, the gains offered by high-level languages are usually made at the cost of reduced performance: higher-level languages usually consume more memory, run more slowly and require expensive garbage-collecting runtime systems. This trend has been worsening with the increasing adoption of the functional programming paradigm by the industry. Modern programmers are thus faced with a dilemma: should they favor productivity and lower maintenance costs at the expense of performance, or should they focus on performance, to the detriments of almost everything else? The main idea behind this thesis is that we can help solve this dilemma by making advances in type systems, metaprogramming, and compilers technology. In particular, we study how metaprogramming via statically-typed quasiquotation can let programmers define their own domain-specific optimizations in a safe way, while leveraging the latest advances in intermediate program representations. We present the design and implementation of the Squid metaprogramming framework, which extends the Scala programming language with multi-staged programming capabilities and more. We also present different application examples for Squid, including a polymorphic yet efficient library for linear algebra, a stream fusion engine improving on the state of the art, a demonstration of query compilation by rewriting, a staged SQL database system prototype, and a new embedded domain-specific language for expressing queries over collections of data.

EPFL2020

Verified Functional Programming

Nicolas Charles Yves Voirol

EPFL2019