One of the differences between Brouwerian intuitionistic logic and classical logic is their treatment of time. In classical logic truth is atemporal, whereas in intuitionistic logic it is time-relative. Thus, in intuitionistic logic it is possible to acquire new knowledge as time progresses, whereas the classical Law of Excluded Middle (LEM) is essentially flattening the notion of time stating that it is possible to decide whether or not some knowledge will ever be acquired. This paper demonstrates that, nonetheless, the two approaches are not necessarily incompatible by introducing an intuitionistic type theory along with a Beth-like model for it that provide some middle ground. On one hand they incorporate a notion of progressing time and include evolving mathematical entities in the form of choice sequences, and on the other hand they are consistent with a variant of the classical LEM. Accordingly, this new type theory provides the basis for a more classically inclined Brouwerian intuitionistic type theory.

Proving the absence of bugs in a given piece of software (a problem which has been known to be intrinsically hard since Turing and Cook) is not the only challenge in software development. Indeed, the ever growing complexity of software increases the need for more trustable optimisations. Solving these two problems (reliability, optimisation) implies the development of safe (without false negative answers) and efficient (wrt memory and time) analyses, yet precise enough (with few false positive answers).

In this talk I will present two experiences in the design of static analyses dedicated to array properties and explore the intrinsic difficulties we, together with my coauthors, faced while developing them. I will also show some experimental evidence of the impact of this work on real-world compilers, as well as future perspective for this area of research.

Research in the field of programming languages traditionally relies on a definition of syntax modulo renaming of bound variables, with its associated operational semantics. We are interested in mathematical tools allowing us to automatically generate syntax and semantics from basic data. We pay particular attention to the notion of substitution, using the categorical notions of monads and modules over them. Languages with variable binding, such as the pure lambda calculus, are monads on the category of sets. We provide a further notion of transition monads which takes into account the operational semantics. We give examples of specifications for transition monads, in the spirit of Initial Semantics, where an object is characterized by some initiality property in a suitable category of models.

From a programmer's perspective, quantum algorithms are simply classical algorithms having access a special kind of memory featuring particular operations: quantum operations. They therefore feature two kinds of control flow. One is purely conventional and is concerned in the classical part of the algorithm. The other – dubbed quantum control – is more elusive and still subject to debate: if the notion of quantum test is reasonably consensual, the quantum counterpart of loops is still not believed to be meaningful.

In this talk, we argue that, under the right circumstances, a reasonable notion of quantum loop is possible. To this aim, we propose a typed, reversible language with lists and fixpoints, extensible to linear combinations of terms. The language admits a reduction strategy in the spirit of algebraic lambda-calculi. Under the restriction of structurally recursive fixpoints, it is shown to capture unitary operations. It is expressive enough to represent several of the unitaries one might be interested in expressing.

As quantum programming is leaving the domain of fiction to join reality, we need to generalise previous work on denotational semantics to the quantum realm. In this talk, we will focus on the semantics for higher order quantum programming languages, namely the pre-existing static model from Pagani, Selinger and Valiron relying on relational semantics, and our dynamic model relying on concurrent game semantics.

In this talk I will present a fully diagrammatic approach to the theory of finite-state automata, based on reinterpreting their usual state-transition graphs as string diagrams. Moreover, I will give an equational theory that completely axiomatises language equivalence in this new setting. The proposed axiomatisation is finitary— a result which is provably impossible to obtain for the usual one-dimensional syntax of regular expressions. This is joint work with Fabio Zanasi.

In a recent article, my students and I have introduced a type-based analysis for deriving upper bounds on the expected execution cost of functional probabilistic programs. The analysis is naturally compositional, parametric in the cost model, and supports higher-order functions and inductive data types. The derived bounds are multivariate polynomials that are functions of data structures. Bound inference is enabled by local type rules that reduce type inference to linear constraint solving. The type system is based on the potential method of amortized analysis and extends automatic amortized resource analysis (AARA) for deterministic programs.

In this talk, I will first give an overview of AARA for deterministic programs and some of the innovations that have been introduced over the past decade. I will then describe our novel results on expected bound analysis for probabilistic programs, highlight the challenges of adopting AARA to a probabilistic language, present experimental results, and discuss some open problems.

Using finite domains to interpret semantically the simply typed lambda-calculus extends naturally the theory of finite state automata to simple programs. In this talk we are going to survey several applications of this approach ranging from equations solving, parsing and model checking.

- Nicolas Behr: Rewriting Theory for the Life Sciences - Camille Combe: Combinatoire des permutations généralisées, des objets Fuss-Catalan et structures algébriques associées. - Hugo Moeneclaey: tba - Sylvain Douteau: Stratified homotopy theory

Au programme de cette deuxième session en ligne des journées de rentrée du pôle PPS:

- Hugo Herbelin: présentation des axes scientifiques du pôle PPS.

- Vincent Blazy: Structure fine du Sous-Typage d’Univers en CCI et applications à la certification de programmes et aux Fondements des Mathématiques.

- Zeinab Galal: A Profonctorial Finiteness Semantics;

- Farzad Jafar-Rahmani: Denotational semantics of logic with fixed points.

- Ada Vienot: tba

Au programme de cette première session en ligne des journées de rentrée de PPS:

- Kostia Chardonnet: Towards a Curry-Howard Correspondence for Quantum Computation

- El-Mehdi Cherradi: Preuves, programmes et homotopie

- Simon Forest: Des constructions génériques pour les catégories supérieures

- Mickael Laurent: Intégration d'outils de programmation avancés dans un langage avec types ensemblistes

The benefits of modularity in programming — abstraction barriers, which allows hiding implementation details behind an opaque interface, and genericity, which allows specializing a single implementation to a variety of underlying data types — apply just as well to deductive program verification, with the additional advantage of helping the automated proof search procedures by reducing the size and complexity of the premises and by instantiating and reusing once-proved properties in a variety of contexts.

This talk presents the modularity features of WhyML, the language of the program verification tool Why3. Instead of separating abstract interfaces and fully elaborated implementations, WhyML uses a single concept of “module”, a collection of abstract and concrete declarations, and a basic operation of “cloning” which instantiates a module with respect to a given partial substitution, while verifying its soundness. This mechanism brings into WhyML both abstraction and genericity, as illustrated by a small verified Bloom filter implementation, translated into executable idiomatic C code.

We introduce a lambda-calculus decorated with types, enhanced with intersection types, union types, and dependent types. Intersection and union types are a way to express ad hoc polymorphism and are an alternative to the parametric polymorphism of Girard. Dependent types were introduced as a way to formalize intuitionistic logic using the “proofs-as-lambda-terms / formulae-as-types” Curry-Howard principle. The resulting type system can be enriched with a decidable subtyping relation. We then discuss the design decisions which have led us to the formulation of these calculi, and provide some examples of applications; and we finally present a software implementation of the Delta-framework, with a description of the type checker, the refinement algorithm, the subtyping algorithm, the evaluation algorithm and the command-line interface. This work can be understood as a little step toward an alternative type theory to defining polymorphic programming languages and interactive proof assistants.

We will present 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 many projects of the DeepSpec ecosystem, making them a convenient 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 this talk, we will particularly focus on how ITrees can be used in the context of verified compilation. To this end, we will first introduce the core concepts over a toy language, before sketching how we have been scaling the approach to LLVM IR as part of the Vellvm DeepSpec project.

Concurrent Kleene algebra (CKA) is an algebraic framework to reason about concurrent programs. In recent years, we have studied several ways of enhancing CKA with extra features, to carry out more sophisticated verification tasks.

In this talk, I will start by recalling the basic definitions of CKA, and its decidability and completeness theorems. We will then take an overview of some of its extensions, considering aspects such as control-flow, memory consistency and mutual exclusion.

This talk is the result of collaborations with Tobias Kappé, Jana Wagemaker, Simon Docherty, Fabio Zanasi, Jurriaan Rot, Alexandra Silva, David Pym, Damien Pous, and Georg Struth.

Separation logic has proven an effective way of reasoning about functional correctness of imperative programs. In the last decade, tools brought its expressiveness to interactive program verification (for example, CFML applies to a meaningful fragment of the OCaml language).

There is now a call for reasoning principles for shared-memory concurrency. In real-world applications, shared memory typically exhibits counter-intuitive behaviors, and “weak” memory models are required to describe them. This poses specific challenges for program verification.

After introducing the weak memory model of Multicore OCaml, I will derive a program logic for this language, and demonstrate its usage on simple examples.

I will show how, in our logic, the invariants of these concurrent data structures extend from the naive model of memory to the weaker model enforced by Multicore OCaml. This model is simpler than that of C11, and we argue that our logic exhibits primitive reasoning principles that are easier to deal with than what was possible for C11.

This work builds on the Iris concurrent separation logic framework and is fully mechanized in Coq.

The security of communications heavily relies on cryptography. For decades, mathematicians have invested an immense effort in providing cryptography that is built on firm mathematical foundations. This has lead to a collection of cryptographic primitives whose correctness can be proved by drawing on results from branches of mathematics such as complex analysis, algebraic geometry, representation theory and number theory. A stated goal of recent competitions for cryptographic standards is to gain trust from the broad cryptography community through open and transparent processes. These processes generally involve open-source reference and optimized implementations for performance evaluation, rigorous security analyses for provable security evaluation and, often, informal evaluation of security against side-channel attacks. These artefacts contribute to building trust in candidates, and ultimately in the new standard. However, the disconnect between implementations and security analyses is a major cause for concern.

In this talk, I will present the Jasmin-EasyCrypt project that explores how formal approaches could eliminate this disconnect and bring together implementations (most importantly, efficient implementations) and software artefacts, in particular machine-checked proofs, supporting security analyses.

Suite de l'exposé de la semaine précédente, cf. son résumé.

Nous donnerons un panorama « généraliste » des différentes variantes de la théorie des types de Martin-Löf et de leurs implémentations dans des assistants de preuve (Agda, Coq, Lean, Arend, …). En particulier, nous essaierons d'articuler certaines questions autour des questions d'égalité définitionnelle/propositionnelle, conversion judgementale/non-typée, univers à la Tarski/Russell, syntaxe intrinsèque/extrinsèque.

Nous donnerons les principes de base de la manière de pensée « HoTT » : principle d'univalence (= extensionalité des types), inductifs supérieurs (généralisation des pushouts), niveaux d'homotopie (h-niveaux), correspondance entre preuves d'égalité et chemins, correspondance propositions/types/espaces/∞-groupoïdes, description « synthétique » d'espaces géométriques (par exemple, cercle = pure donnée algébrique d'un point et d'un chemin autour de ce point), construction de Grothendieck reliant ΣB.(B→A) et A→Type.

Nous pourrions aussi aborder la théorie des types cubiques vue comme style direct pour la paramétricité itérée délimitée. Nous pourrions aussi essayer d'ébaucher le dictionnaire permettant de connecter les vocabulaires informatique/logique/géométrique/catégorique.

À noter que l'exposé essaiera en premier lieu de répondre à la curiosité de l'auditoire et le plan donné pourra évoluer en fonction des questions posées.

To verify properties of functional programs, such as termination, one can use for instance type theory or model-checking. I will present some results for the verification of functional programs, both in the deterministic and in the probabilistic case. In the deterministic case, model-checking of formulas of monadic second-order logic (MSO) is decidable over higher-order recursion schemes (HORS), a candidate model for functional programs. I will present this result, and then turn to the probabilistic case, for which we will explore two approaches for verifying termination: one based on type theory, the other one on model-checking.

Very short abstract: What is an existentially closed Heyting algebra and what does it have to do with automata theory?

Slightly longer abstract: Logical systems of deduction often resemble algebraic systems of equation resolution. The simplest instance of this resemblance is the fact that classical propositional logic essentially boils down to studying algebras over the two-element field. When one changes the logical deduction system, the algebraic structures become less simple, and more interesting; this is where one enters the world of Heyting algebras, modal algebras, and generalizations of such.

The aim of our work here is to gain a better understanding of such logical-algebraic structures by studying them from the perspective of model theory. In the model-theoretic study of usual algebra, the concept of model completeness plays a central role: it provides the correct abstraction of the concept of an algebraically closed field. We show that model completeness also has an important role to play in logical algebra.

In particular, we will discuss two cases of model completeness: intuitionistic logic, and linear temporal logic. In the former, model completeness can be seen to be closely related to a certain interpolation property of the logic, originally established by Pitts. In the latter, automata on infinite words are the technical ingredient that leads to model completeness.

On introduit les systèmes de réécriture topologiques comme généralisation des systèmes de réécriture abstraits, où l'on considère un espace topologique au lieu d'un ensemble de termes. Les systèmes de réécriture abstraits sont les systèmes de réécriture topologiques pour la topologie discrète. On introduit la confluence topologique comme étant une propriété de confluence par passage à la limite, et on caractérise les bases standards par cette propriété. On caractérise également la confluence topologique par des opérations de treillis grâce à une représentation des systèmes de réécriture par des opérateurs de réduction continus. Enfin, on relie les représentations des séries formelles non commutatives à la dualité des opérateurs de réduction, et on déduit un critère pour qu'une algèbre soit syntaxique.

I will talk about a system that combines Dependent Types and Linear Types. As an application of this system, I will show how to transport Martin Hofmann's LFPL and Amortised Resource analysis systems for resource constrained computing to full dependent types. This results in a theory where unconstrained computations are allowed at the type level, but only polynomial time computations at the term level. The combined system now allows one to explore the world of propositions whose proofs are not only constructive, but also of restricted complexity.

Systems programming often requires the manipulation of resources like file handles, network connections, or dynamically allocated memory. Programmers need to follow certain protocols to handle these resources correctly. Violating these protocols causes bugs ranging from type mismatches over data races to use-after-free errors and memory leaks. These bugs often lead to security vulnerabilities.

While statically typed programming languages guarantee type soundness and memory safety by design, most of them do not address issues arising from improper resource handling. Linear and affine types guarantee single-threaded resource usage, but they are rarely deployed as they are too restrictive for real-world applications.

We present Affe, an extension of ML with constrained types that manages linearity and affinity properties through kinds. In addition Affe supports the exclusive and unrestricted borrowing of affine resources, inspired by features of Rust. Moreover, Affe retains the defining features of the ML family: an impure, strict functional expression language with complete principal type inference and type abstraction through modules. Our language does not require any linearity annotations in expressions and supports common functional programming idioms.

Draft: https://arxiv.org/abs/1908.09681

Despite continued progress in program verification, many fundamental data structures and algorithms remain difficult to verify. Challenges arise when programs use concurrency or randomization because these effects lead to non-deterministic behavior. Although many specialized logics have been developed to reason about programs that use either concurrency or randomization, most can only handle the use of one of these features in isolation. However, many common concurrent data structures are randomized, making it important to consider the combination.

This talk will describe Polaris, a logic for reasoning about programs that are both concurrent and randomized. Polaris combines ideas from three separate lines of work: (1) Varacca and Winskel's denotational model of non-determinism and probability, (2) Barthe et al.'s approach to probabilistic relational reasoning via couplings, and (3) higher-order concurrent separation logic, as realized in the Iris verification framework.