The DeepSpec research project is a cross institution, cross project investigation to push further the science of specification and verification of software artifacts. Its ambition is crystallized into four qualities that specifications should have: they should be rich, live, two-sided and formal.

In this talk, we will focus on the design and implementation of Interaction Trees (ITrees), a general-purpose data-structure for representing in Coq potentially divergent, effectful, programs. ITrees are built out of uninterpreted events and their continuations. They support compositional construction of interpreters from event handlers, which give meaning to events by defining their semantics as monadic actions. They are expressive enough to represent impure and potentially nonterminating, mutually recursive computations in Coq. Finally, they give rise to a theory enabling equational reasoning, up to weak bisimulation, about ITrees and monadic computations built from them. In contrast to other approaches, ITrees are executable via code extraction.

ITrees are expressive enough to serve as a language of specification for most projects of the DeepSpec ecosystem, making them a sort of Franca Lingua for formal specification, and helping in connecting projects together. Furthermore, their ability to be extracted make them compatible with ambitions of liveness and two-sidedness.

In a second part of this talk, we will focus on how ITrees are used in one of the DeepSpec projects in particular: Vellvm. More specifically, we will give an account of the ongoing effort to use ITrees as a mean to define a modular formal semantics of LLVM IR.

Accessible categories with directed colimits have proven to be a suitable framework to develop abstract model theory and generalize the notion of abstract elementary class, quite relevant in model theory. For every accessible category with directed colimits A, one can define its Scott topos S(A). This construction is the categorification of the Scott topology over a poset with directed unions, and thus provides a geometric understanding of accessible categories. S(A) represents also a candidate axiomatization of A, in the sense that the category of points of the Scott topos (i.e., the models of the theory that it classifies) is very often a relevant hull of A. During the talk we introduce the Scott construction and explain both its geometric and logical aspects.

We describe a dependent type theory, and a denotational model for it, that incorporates both intensional and extensional semantic universes. In the former, terms and types are interpreted as strategies on certain graph games, which are concrete data structures of a generalized form, and in the latter as stable functions on event domains. The concrete data structures themselves form an event domain, with which we may interpret an (extensional) universe type of (intensional) types. A dependent game corresponds to a stable function into this domain; we use its trace to define dependent product and sum constructions as it captures precisely how unfolding moves combine with the dependency to shape the possible interaction in the game. Since each strategy computes a stable function on CDS states, we can lift typing judgements from the intensional to the extensional setting, giving an expressive type theory with recursively defined type families and type operators. We define an operational semantics for intensional terms, giving a functional programming language based on our type theory, and prove that our semantics for it is computationally adequate. By extending it with a simple non-local control operator on intensional terms, we can precisely characterize behaviour in the intensional model. We demonstrate this by proving full abstraction and full completeness results.

Inductive datatypes in programming languages allow users to define useful data structures such as natural numbers, lists, trees, and others. In this talk we discuss how inductive datatypes may be added to the quantum programming language QPL. We construct a sound categorical model for the language and by doing so we provide the first detailed semantic treatment of user-defined inductive datatypes in quantum programming. We also show our denotational interpretation is invariant with respect to big-step reduction, thereby establishing another novel result for quantum programming. Compared to classical programming, this property is considerably more difficult to prove and we demonstrate its usefulness by showing how it immediately implies computational adequacy at all types. To further cement our results, our semantics is entirely based on a physically natural model of von Neumann algebras, which are mathematical structures used by physicists to study quantum mechanics. Joint work with Romain Péchoux, Simon Perdrix and Mathys Rennela.

Finite-precision floating point arithmetic introduces rounding errors which are traditionally bounded using a worst-case analysis. However, worst-case analysis might be overly conservative because worst-case errors can be extremely rare events in practice. Here we develop a probabilistic model of rounding errors with which it becomes possible to quantify the likelihood that the rounding error of an algorithm lies within a given interval.

Given an input distribution, the model requires the distribution of rounding errors. We show how to exactly compute this distribution for low precision arithmetic. For high precision arithmetic we derive a simple but surprisingly useful approximation. The model is then entirely compositional: given a numerical program written in a simple imperative programing language we can recursively compute the distribution of rounding errors at each step and propagate it through each program instruction. This is done by applying a formalism originaly developed by Kozen to understand the semantics of probabilistic programs, for example how probability distributions gets transformed by assignments or “if then else” statements.

The μ-calculus with atoms, or nominal μ-calculus, is a temporal logic for reasoning about transition systems that operate on data atoms coming from an infinite domain and comparable only for equality. It is, however, not expressive enough to define some properties that are of interest from the perspective of system verification. To rectify this, we extend the calculus with tests for atom freshness with respect to the global history of transitions. Since global histories can grow arbitrarily large, it is not clear whether model checking for the extended calculus is decidable. We prove that it is, by showing that one can restrict attention only to locally relevant parts of the history.

Recursion is a great tool to create readable programs and for proof discovery. Unrestricted recursion, however, leads to non-termination and thereby makes reasoning about programs harder and may make a logic inconsistent. Guarded recursion, on the other hand, allows us to control recursion in programs and proofs. The basic idea is to extend types or formulas with a modality, usually called the later modality, and a few rules that allow the controlled introduction of recursion. This control ensures termination of programs and consistency of proofs.

In this talk, I will first show how a fibration can be extended, under mild conditions, to a fibration with guarded recursion. The abstract settings of fibrations allows the application of guarded recursion in various settings such as probabilistic programming and reasoning. We will see this in the second part of the talk in action, where we will devise a language for coinductive probabilistic processes based on guarded recursion that retains termination. The semantics of this language is obtained by applying the construction from the first part of the talk to quasi-Borel spaces. This gives an alternative language with guaranteed termination to the probabilistic language with unrestricted recursion recently given by Vákár et al. (POPL'19).

There are different categorical approaches to variations of transition systems and their bisimulations. One is coalgebras, another one is open maps. In this talk, I will describe these two approaches, illustrated by the case of labelled transition systems (almost no knowledge in category theory is needed for this part). I will then describe how it is possible to translate one into the other in some cases. From open maps to coalgebras, this was done by Lasota, using multi-sorted transition systems. From coalgebras to open maps, this was done in my joint work with Thorsten Wißmann, Shin-ya Katsumata and Ichiro Hasuo, where we derived path-categories and trace semantics for free for different flavors of categories of coalgebras with non-deterministic branching. I will illustrate those constructions on various concrete examples (tree automata, regular nominal automata, …).

We introduce a new type of algebra, the Expedient Algebra EXP, for which computations satisfy tight distribution control. Algorithms satisfying such distribution control are guaranteed to support modular time analysis–drastically simplifying static timing. The property ensures that problematic algorithms, for which the exact time is too hard or impossible to analyze with current means can be distinguished at code level from algorithms supporting an elegant modular time analysis. Little is known about the intrinsic properties of algorithms exhibiting such distribution control.

We show that EXP-computations, made reversible through history-keeping, act as closed systems in which entropy is conserved. Thus modularity of timing is linked to entropy conservation of data flow, sharpening traditional entropy preservation guaranteed by the second law of thermodynamics for reversible systems. This type of conservation typically holds for the case of energy, but not for entropy. A salient point is that for algorithms satisfying distribution control, entropy is neither created nor destroyed, merely transferred from one form, i.e. quantitative entropy, to another, i.e. positional entropy.

We establish the Entropy Conservation Laws ECL-1 and ECL-2. ECL-1 expresses the inverse proportionality of positional and quantitative entropy for distributions over series-parallel orders and their duals. ECL-2, a computational version of entropy conservation, expresses that order established by the expedient product (with history) on labels is proportionally destroyed on indices by a shadow transformation in the dual space. The laws shed new light on the properties of algorithms for which distribution control, and hence modular timing, is guaranteed.

La traduction naïve des structures ensemblistes dans la théorie des types de Martin-Lof est souvent incomplète: sans hypothèses auxiliaires, comme la decidabilité de l'égalité ou troncation, ces traductions ne spécifient pas le comportement de la structure par rapport aux égalités supérieures. Par contre, une description complète n'est pas facile puisque celle-ci exige un nombre infini d'équations. Je présenterai des progrès récent sur ce problème en donnant une définition d'une “monade polynomiale” interne à la théorie des types.

The talk gives an overview of our several works on programming language Go

POPL'17 Fencing off go: liveness and safety for channel-based programming ICSE'18 A Static Verification Framework for Message Passing in Go using Behavioural Types POPL'19 Distributed Programming Using Role Parametric Session Types in Go.

Go is a production-level statically typed programming language whose design features explicit message-passing primitives and lightweight threads, enabling (and encouraging) programmers to develop concurrent systems where components interact through communication more so than by lock-based shared memory concurrency. Go can detect global deadlocks at runtime, but does not provide any compile-time protection against all too common communication mismatches and partial deadlocks. We present a static verification framework for liveness and safety in Go programs, able to detect communication errors and deadlocks by model checking. Our toolchain infers from a Go program a faithful representation of its communication patterns as behavioral types, where the types are model checked for liveness and safety. We also present a recent code generation for Go.

A cornerstone of the theory of λ-calculus is that intersection types characterise termination properties. They are a flexible tool that can be adapted to various notions of termination, and that also induces adequate denotational models. Since the seminal work of de Carvalho in 2007, it is known that multi types (i.e. non-idempotent intersection types) refine intersection types with quantitative information and a strong connection to linear logic. Typically, type derivations provide bounds for evaluation lengths, and minimal type derivations provide exact bounds. De Carvalho studied call-by-name evaluation, and Kesner used his system to show the termination equivalence of call-by-need and call-by-name. De Carvalho’s system, however, cannot provide exact bounds on call-by-need evaluation lengths. In this paper we develop a new multi type system for call-by-need. Our system produces exact bounds and induces a denotational model of call-by-need, providing the first tight quantitative semantics of call-by-need.

We present a denotational semantics for higher-order probabilistic programs in terms of linear operators between Banach spaces. Our semantics is rooted in the classical theory of Banach spaces and their tensor products, but bears similarities with the well-known semantics of higher-order programs à la Scott through the use ordered Banach spaces which allow definitions in terms of fixed points. Being based on a monoidal rather than cartesian closed structure, our semantics effectively treats randomness as a resource.

Je rappelle, pour fixer les notations, que si S est une catégorie, et F: S° —> CAT est un lax foncteur, cette construction fournit une catégorie Gr(F) munie d’une préfibration Pr(F): Gr(F)—>S qui est une fibration ssi F est un pseudo-foncteur. Questions: Par quel type de bi, ou 2, catégorie K peut on remplacer CAT ? Quelles propriété a la correspondance F —> Gr(F) Peut-on internaliser cette construction i.e. si E est, par exemple, un topos, peut-on remplacer S par une catégorie interne à E et CAT par la 2-catégorie CAT(E) des catégories internes à E. La liste ci-dessus est loin d’être exhaustive. Je tâcherai, sans lasser l’auditoire, de montrer la grande variété des questions…, et des réponses.