Programming Languages

Actor coordination armoured with a suitable protocol description language has been a pressing problem in the actors community. We study the applicability of multiparty session type (MPST) protocols for verification of actor programs. We…

Constraint automata (CA) constitute a coordination model based on finite automata on infinite words. Originally introduced for modeling of coordinators, an interesting new application of CAs is implementing coordinators (i.e., compiling CAs…

We study the semantic meaning of block structure using game semantics. To that end, we introduce the notion of block-innocent strategies and characterise call-by-value computation with block-allocated storage through soundness, finite…

We extend the linear {\pi}-calculus with composite regular types in such a way that data containing linear values can be shared among several processes, if there is no overlapping access to such values. We describe a type reconstruction…

We propose a type system for a calculus of contracting processes. Processes can establish sessions by stipulating contracts, and then can interact either by keeping the promises made, or not. Type safety guarantees that a typeable process…

We prove that orthogonal constructor term rewrite systems and lambda-calculus with weak (i.e., no reduction is allowed under the scope of a lambda-abstraction) call-by-value reduction can simulate each other with a linear overhead. In…

We present a static analysis by Abstract Interpretation to check for run-time errors in parallel and multi-threaded C programs. Following our work on Astr\'ee, we focus on embedded critical programs without recursion nor dynamic memory…

According to Strachey, a polymorphic program is parametric if it applies a uniform algorithm independently of the type instantiations at which it is applied. The notion of relational parametricity, introduced by Reynolds, is one possible…

The rapid evolution of deep neural networks is demanding deep learning (DL) frameworks not only to satisfy the requirement of quickly executing large computations, but also to support straightforward programming models for quickly…

This paper presents reverse-mode algorithmic differentiation (AD) based on source code transformation, in particular of the Static Single Assignment (SSA) form used by modern compilers. The approach can support control flow, nesting,…

Noisy, intermediate-scale quantum (NISQ) systems are expected to have a few hundred qubits, minimal or no error correction, limited connectivity and limits on the number of gates that can be performed within the short coherence window of…

Despite advancements in the areas of parallel and distributed computing, the complexity of programming on High Performance Computing (HPC) resources has deterred many domain experts, especially in the areas of machine learning and…

We introduce Meta-F*, a tactics and metaprogramming framework for the F* program verifier. The main novelty of Meta-F* is allowing the use of tactics and metaprogramming to discharge assertions not solvable by SMT, or to just simplify them…

TensorFlow Eager is a multi-stage, Python-embedded domain-specific language for hardware-accelerated machine learning, suitable for both interactive research and production. TensorFlow, which TensorFlow Eager extends, requires users to…

Graph algorithms are at the heart of several applications, and achieving high performance with them has become critical due to the tremendous growth of irregular data. However, irregular algorithms are quite challenging to parallelize…

We define an abstract framework for object-oriented programming and show that object-oriented languages, such as C++, can be interpreted as parallel programming languages. Parallel C++ code is typically more than ten times shorter than the…

In this paper we use pre existing language support for type modifiers and object capabilities to enable a system for sound runtime verification of invariants. Our system guarantees that class invariants hold for all objects involved in…

Building reliable applications for the cloud is challenging because of unpredictable failures during a program's execution. This paper presents a programming framework called Reliable State Machines (RSMs), that offers fault-tolerance by…

Automatic (i.e., computer-assisted) theorem proving (ATP) can come in many flavors. This document presents early steps in our effort towards defining object-oriented theorem proving (OOTP) as a new style of ATP. Traditional theorem proving…

This paper is a contribution to exploring and analyzing space-improvements in concurrent programming languages, in particular in the functional process-calculus CHF. Space-improvements are defined as a generalization of the corresponding…