Contextual equivalence is a relation over program expressions which guarantees that related expressions are interchangeable in any program context. It encompasses verification properties like safety and termination, has attracted considerable attention from the semantics community, and has found its main applications in the verification of cryptographic protocols, compiler correctness and regression verification.

In this talk we present a bounded equivalence verification technique for higher-order programs with local state. This technique combines fully abstract symbolic environmental bisimulations similar to symbolic game semantics, up-to techniques, and lightweight state invariant annotations. This yields an equivalence verification technique with no false positives or negatives. The technique is bounded-complete, in that all inequivalences are automatically detected given large enough bounds. Moreover, several hard equivalences are proved automatically or after being annotated with state invariants. We have realised the technique in a tool prototype called Hobbit and benchmarked it with an extensive set of new and existing examples. Hobbit can prove many classical equivalences including all Meyer and Sieber examples.

Epistemic Logic is the modal logic of knowledge. It allows to reason about a finite set of agents who can know facts about the world, and about what the other agents know. The traditional Kripke-style semantics for epistemic logic is based on graphs whose vertices represent the possible worlds, and whose edges indicate the agents that cannot distinguish between two worlds. In this talk, I will present an alternative semantics for epistemic logic, based on combinatorial topology. The idea is to replace the Kripke graph by a simplicial complex, allowing for higher-dimensional connectivity between the possible worlds. In fact, every Kripke model can be turned into an equivalent simplicial model, thus uncovering its underlying topological information.

This is joint work with Éric Goubault and Sergio Rajsbaum

Necula (PLDI'2000) and Tristan, Gouvereau, Morrisett (PLDI'2011) established that symbolic execution combined with rewriting is effective in validating the code produced by state-of-the-art compilers applying various optimizations. In the meantime, Tristan and Leroy (POPL'2008) used formally-verified symbolic execution to certify the schedules produced by untrusted oracles – optimizing pipeline usage – within the CompCert compiler. Alas, their formally-verified checker had exponential complexity and was thus never integrated into mainline CompCert.

With Cyril Six and David Monniaux, we solved this performance issue with formally verified hash-consing within the symbolic execution. And we successfully applied this technique to implement within CompCert effective optimizations targeting superscalar (or VLIW) in-order processors.

The talk will actually start by briefly introducing a sound Foreign Function Interface for embedding OCaml oracles within Coq. Hence, it will explain how we used it in this application.

Law at large underpins modern society, codifying and governing many aspects of citizens' daily lives. Oftentimes, law is subject to interpretation, debate and challenges throughout various courts and jurisdictions. But in some other areas, law leaves little room for interpretation, and essentially aims to rigorously describe a computation, a decision procedure or, simply said, an algorithm. Unfortunately, prose remains a woefully inadequate tool for the job. The lack of formalism leaves room for ambiguities; the structure of legal statutes, with many paragraphs and sub-sections spread across multiple pages, makes it hard to compute the intended outcome of the algorithm underlying a given text; and, as with any other piece of poorly-specified critical software, the use of informal language leaves corner cases unaddressed. We introduce Catala, a new programming language that we specifically designed to allow a straightforward and systematic translation of statutory law into an executable implementation. Catala aims to bring together lawyers and programmers through a shared medium, which together they can understand, edit and evolve, bridging a gap that often results in dramatically incorrect implementations of the law. We have implemented a compiler for Catala, and have proven the correctness of its core compilation steps using the F* proof assistant. We evaluate Catala on several legal texts that are algorithms in disguise, notably section 121 of the US federal income tax and the byzantine French family benefits; in doing so, we uncover a bug in the official implementation. We observe as a consequence of the formalization process that using Catala enables rich interactions between lawyers and programmers, leading to a greater understanding of the original legislative intent, while producing a correct-by-construction executable specification reusable by the greater software ecosystem.

Modern software increasingly exploits parallelism to reach new heights of performance. Unfortunately, concurrent programming is error-prone, and developers often make incorrect assumptions about how their programs will behave, raising concerns about its use in critical systems. Using formal methods to provide strong correctness guarantees is appealing, but challenging; verification frameworks either lack the expressivity required to model every advanced low-level pattern found in real-world implementations, or they do not retain the level of automation needed to ensure the scalability of verification. To address this issue, we present Steel, a new verification framework to develop and prove concurrent programs embedded in F*, a dependently typed programming language and proof assistant.

In this talk, we give an overview of Steel from the ground up. To reason about programs, Steel provides a higher-order, impredicative concurrent separation logic with support for dynamically-allocated invariants and partial commutative monoids (PCMs). To automate verification, Steel separates verification conditions between separation logic predicates and first-order logic encodeable predicates; we develop a (partial) decision procedure using efficient, reflective tactics that focuses on the former, while the latter can be encoded efficiently to SMT by F*. We will conclude by presenting several verified Steel libraries, including mutable, self-balancing trees as well as a novel PCM-based encoding of 2-party dependently typed sessions, that illustrate the expressiveness and programmability of Steel.

The chef kicks them out: “I'm sorry, in my kitchen we only use induction”

This talk will start from Morris' PhD thesis in 1968 and present 50 years of theoretical computer science, through PCF, CCS, Alternating transition systems, contexts and strategies, ending up at the footsteps of the monumental Palace of Justice in Créteil.

Informally, “constructivism” is a programme of mathematics aiming to ensure that anything asserted to exist must be explicitly constructed. It is generally practiced using intuitionistic logic, which achieves this by rejecting the law of excluded middle. However, the same result is also achieved by Girard's linear logic, which instead restricts the number of times each hypothesis can be used in a proof; but essentially no practicing constructivists today use linear logic.

I will show that intuitionistic and linear approaches to constructive mathematics are intimately connected, through an interpretation of linear logic (or more precisely, affine logic) into intuitionistic logic based on a categorical Chu/Dialectica construction called the “antithesis translation”. In particular, many odd features of intuitionistic mathematics, such as inequality relations, anti-subgroups, and apartness spaces, arise automatically and unavoidably by translating natural definitions from affine logic across this interpretation. Thus, affine logic can be used as a “high-level tool” for intuitionistic mathematics, helping to find the right definitions and manage the bookkeeping of formally dual properties in proofs.

Focusing is a general technique for syntactically compartmentalising the non-deterministic choices in a proof system, which not only improves proof search but also has the representational benefit of distilling sequent proofs into synthetic normal forms. However, since focusing was traditionally specified as a restriction of the sequent calculus, the technique had not been transferred to logics that lack a (shallow) sequent presentation, as is the case for some modal or substructural logics.

With K. Chaudhuri and L. Straßburger, we extended the focusing technique to nested sequents, a generalisation of ordinary sequents which allows us to capture all the logics of the classical and intuitionistic S5 cube in a modular fashion. This relied, following the method introduced by O. Laurent, on an adequate polarisation of the syntax and an internal cut-elimination procedure for the focused system which in turn is used to show its completeness.

Recently, with A. Gheorghiu, we applied a similar method to the logic of Bunched Implications (BI), a logic that freely combines intuitionistic logic and multiplicative linear logic. For this we had first to reformulate the traditional bunched calculus for BI using nested sequents, followed by a polarised and focused variant that (again) we show is sound and complete via a cut-elimination argument.

Game semantics is the art of interpreting formulas (or types) as games and proofs (or programs) as strategies. In order to reflect the interactive behaviour of programs, strategies are required to follow specific scheduling policies. Typically, in the case of a sequential programming language, the program (Player) and its environment (Opponent) play one after the other, in a strictly alternating way. On the other hand, in the case of a concurrent language, Player and Opponent are allowed to play several moves in a row, in a non alternating way. In the two cases, the scheduling policy is designed very carefully in order to ensure that the strategies synchronise properly and compose well when plugged together. A longstanding conceptual problem has been to understand when and why a given scheduling policy works and is compositional in that sense. In this talk, I will introduce the notion of template game and exhibit a number of simple and fundamental combinatorial properties which ensure that a given scheduling policy defines (indeed) a monoidal closed bicategory of games, strategies and simulations. The notion of template game will be illustrated by constructing two game models of linear logic with different flavours (alternating and asynchronous) using the same categorical combinatorics, performed in the category of small 2-categories.

The interested reader will find more material here https://www.irif.fr/~mellies/template-games.html https://www.youtube.com/watch?v=ZC2jtq2R3cw and in the companion papers [1,2,3].

[1] PAM. Categorical combinatorics of scheduling and synchronization in game semantics. Proceedings of POPL 2019. https://www.irif.fr/~mellies/papers/Mellies19popl.pdf https://www.irif.fr/~mellies/slides/popl-slides-january-2019.pdf

[2] PAM. Template games and differential linear logic. Proceedings of LICS 2019. https://www.irif.fr/~mellies/template-games/2-template-games-and-differential-linear-logic.pdf

[3] PAM. Asynchronous template games and the Gray tensor product of 2-categories. Proceedings of LICS 2021. https://www.irif.fr/~mellies/papers/asynchronous-template-games.pdf

[4] PAM. Une étude micrologique de la négation https://www.irif.fr/~mellies/hdr-mellies.pdf

In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. In the dependently-typed setting, however, we would like to appeal to such invariance results within a language itself, in order to transfer theorems from simple to complex implementations. Homotopy type theorists have noted that Voevodsky's univalence principle equates isomorphic structures, but unfortunately many instances of representation independence are not isomorphisms.

In this talk, we describe a technique for establishing internal relational representation independence results in Cubical Agda by using higher inductive types to simultaneously quotient two related implementation types by a heterogeneous correspondence between them. The correspondence becomes an isomorphism between the quotiented types, thereby allowing us to obtain an equality of implementations by univalence. Joint work with Evan Cavallo, Anders Mörtberg, and Max Zeuner. Available at https://dl.acm.org/doi/10.1145/3434293.

Static analysis aims at discovering semantic properties of software prior to execution. Examples of emantic properties of interest include the absence of some classes of errors, the invariance of certain classes of numerical properties, or the preservation of the shape of unbounded data-structures. While many static analyses proceed by computing an over-approximation of the set of reachable states of a program, it is also possible to seek for an abstraction of the input/output relation of programs. The former is often sufficient to answer questions such as “may my program crash ?”, but the former opens up several interesting roads. First it allows to prove certain classes of functional correctness properties. Second, it makes it possible to reuse the analysis for a given program fragment (typically a function), and to speed up the overall analysis process. We call such analyses relational. However, relational analyses need to manipulate abstractions of state relations. Tables of pairs or abstract pre- and post-conditions are often used. In this talk, we present an abstraction that is based on logical connectors that are designed specifically to capture relations. We present the abstrction, analysis algorithms and examples.

(Joint work with Hugo Illous and Matthieu Lemerre.)

Monads and their presentations via equational theories provide a tool for reasoning about programs with computational effects. In recent works, we have studied monads resulting from the combination of nondeterminism, probabilities, and termination, as well as their extensions to the category of metric spaces. In this talk, we'll introduce this framework and show applications to proving equivalences and distances of nondeterministic and probabilistic systems.

Bibliography:

Bonchi, Sokolova, Vignudelli. The theory of traces for systems with nondeterminism and probabilities. LICS 2019. Available at: https://arxiv.org/abs/1808.00923

Mio, Vignudelli. Monads and quantitative equational theories for nondeterminism and probabilities. CONCUR 2020. Available at: https://arxiv.org/abs/2005.07509

Mio, Sarkis, Vignudelli. Combining nondeterminism, probability, and termination: equational and metric reasoning. LICS 2021. Available at: https://arxiv.org/abs/2012.00382

Knaster-Tarski's theorem, characterising the greatest fixpoint of a monotone function over a complete lattice as the largest post-fixpoint, naturally leads to the so-called coinduction proof principle for showing that some element is below the greatest fixpoint (e.g., for providing bisimilarity witnesses). The dual principle, used for showing that an element is above the least fixpoint, is related to inductive invariants. This talks considers proof rules which are similar in spirit but for showing that an element is above the greatest fixpoint or, dually, below the least fixpoint.

The theory is developed for non-expansive monotone functions on suitable lattices of the form M^Y, where Y is a finite set and M an MV-algebra, and it is based on the construction of (finitary) approximations of the original functions. We show that our theory applies to a wide range of examples, including termination probabilities, behavioural distances for probabilistic automata and bisimilarity. Moreover it allows us to determine original algorithms for solving simple stochastic games.

The work to be presented is in collaboration with Pierre-Évariste Dagand and Lionel Rieg. It studies the computational content of the Fundamental Lemma of classical realizability for the simply-typed lambda-calculus with sums.

(If you are unfamiliar with classical realizability, it might help to think of it as a unary logical relation with an elegant symmetric setup – it originates in studies of classical logic. The talk will gently introduce classical realizability.)

Two salient points of our presentation correspond to folklore ideas that we present as opinionated recommandations, to ourselves and others, of how to give a “modern” presentation of these questions (classical realizability, and in general studying the computational content of a proof device):

1. We present classical realizablity as compilation to Curien-Herbelin style symmetric abstract machine calculi, instead of the Krivine Abstract Machine, to represent realizers. Experts will recognize the polarized reduction rules of Munch-Maccagnoni.

2. To present computation content, we are *not* using extraction of a program from a mathematical-style proof in a proof assistant. That beautiful approach rarely works and it generates ugly code. Instead we *write* the logical argument directly as a program in a dependently-typed (meta)language, and we think about the code we are writing.

Girard's Geometry of Interaction (GOI) can be made concrete by considering it as an implementation technique for functional programs, in particular the lambda calculus. Our work is about the complexity analysis of the abstract machine based on the GOI, the interaction abstract machine (IAM). We have adapted in a non trivial way de Carvalho's non idempotent intersection types so that type derivations completely characterize the time and space complexity of the IAM, thus providing a logical account of the IAM resource usage. Moreover, by the way of the type systems we have introduced, we are able to state some negative results about time and space cost models for the lambda calculus based on the IAM. This is joint work with Beniamino Accattoli and Ugo Dal Lago.

Transiently-powered systems featuring non-volatile memory as well as external peripherals enable the development of new low-power sensor applications. However, as programmers, we are ill-equipped to reason about systems where power failures are the norm rather than the exception. A first challenge consists in being able to capture all the volatile state of the application –external peripherals included– to ensure progress. A second, more fundamental, challenge consists in specifying how power failures may interact with peripheral operations. In a joint work with Rémi Oudin, Delphine Demange, Gautier Berthou and Tanguy Risset, we have proposed a formal specification of intermittent computing with peripherals, an axiomatic model of interrupt-based checkpointing as well as its proof of correctness, machine-checked in the Coq proof assistant. However, this result assumes that the system is able to maintain a shadow copy of the external devices it interacts with. Perhaps surprisingly, this could be an opportunity to adopt an algebraic treatment of external peripherals.

https://www.irif.fr/rencontres/pps2021/index

https://www.irif.fr/rencontres/pps2021/index

The subject of the SMTCoq project is to significantly enhance automation in the Coq proof assistant. At the heart of SMTCoq is a Coq plugin that offers a way to use automatic provers with the same degree of trust as Coq itself. On top of it, we define a framework to progressively encode Coq's logic into first-order logic, through modular and fine-grained logical transformations that can be composed. Our objective is to obtain automatic while expressive tactics for Coq.

In this talk, I will concisely introduce the communication between Coq and external provers, before presenting the new framework of logical transformations. I will report on work in progress of examples of transformations in this framework.

This is joint work with Valentin Blot, Louise Dubois de Prisque and Pierre Vial.

https://www.irif.fr/rencontres/pps2021/index

https://www.irif.fr/rencontres/pps2021/index

Ce travail est un travail commun avec Sylvie Boldo, François Clément Florian Faissole et Vincent Martin dans le cadre du projet DIM-RFSI MILC. La résolution des équations aux dérivées partielles (EDP) est au cœur de nombreux programmes de simulation dans l'industrie et la méthode des éléments finis (MEF) est un outil très utilisé pour leur résolution numérique.

Je présenterai le but à long terme dans lequel s'inscrit ce travail, domaine de la sécurité, de la fiabilité et de la sûreté. Il s'agit de poser les fondements qui nous permettront de prouver la correction d'une bibliothèque implantant la MEF en C++, telle que FELiScE (Finite Elements for Life Sciences and Engineering). Sa vérification formelle augmentera la confiance dans tous les codes qui l'utilisent. Ces travaux sont interdisciplinaires (logique/preuve de programmes/analyse numérique). Ces preuves reposent entre autres sur les bases mathématiques telles que la théorie de la mesure, l'intégrale de Lebesgue, les distributions, les espaces de Sobolev jusqu'à la construction de l'espace fonctionnel L2. Dans cet exposé je m'attarderai sur la formalisation de l'intégrale de Lebesgue pour les fonctions positives.

Monitorability underpins the technique of Runtime Verification because it delineates what properties can be verified at runtime. Although many monitorability definitions exist, few are defined explicitly in terms of the operational guarantees provided by monitors, i.e., the computational entities carrying out the verification. This work views monitorability as a spectrum, where the fewer guarantees that are required of monitors, the more properties become monitorable. Accordingly, I present a monitorability hierarchy based on this trade-off. For regular specifications, I give syntactic characterisations in Hennessy–Milner logic with recursion for its levels. Finally, I map existing monitorability definitions into our hierarchy. This gives a unified framework that makes the operational assumptions and guarantees of each definition explicit and provides a rigorous foundation that can inform design choices and correctness claims for runtime verification tools.

This is joint work with Luca Aceto, Antonis Achilleos, Anna Ingolfsdottir and Karoliina Lehtinen

We start by presenting a local system for linear logic (LL) based on linear nested sequents. Relying on that system, we propose a general framework for modularly describing systems combining, coherently, substructural behaviors inherited from LL with simply dependent multimodalities. This class of systems includes linear, elementary, affine, bounded and subexponential linear logics and extensions of multiplicative additive linear logic (MALL) with normal modalities, as well as general combinations of them.

We then move to the question of giving an interpretation to subexponentials. We will show a game interpretation of affine linear logic with subexponentials, viewing the game as a playground for illuminating semantic intuitions underlying resource conscious reasoning. Interestingly enough, this led to the proposal of new sequent systems for capturing the notions of costs and budget in a fragment of linear logic with subexponentials, thus opening new possibilities for analysing the problem of comparing proofs.

We finish the talk by showing a computational interpretation of subexponentials in the process-as-formula fashion, where process constructors are mapped to logical connectives and computational steps are related to proof steps. In particular, we will show in detail the role of pre-orders in subexponentials for the adequate specification of different modalities in concurrent systems, such as time, space, epistemic and preferences. We end with a discussion about which new models of computation should arise from the extension of the concept of modality in linear logic.

Some interactions between combinatorics and universal algebra through rewrite systems and clone theory are presented. Given a variety $V$ of algebras (presented by generating operations and relations between some of their compositions), a natural question consists in building a combinatorial realization of $V$. This consists in encoding the operations of $V$ in such a way that two equivalent ones have the same representation, and in providing an algorithm to compute the representation of the functional composition of several operations. In particular, we present a class of clones obtained from monoids. This gives rise among other to realizations of varieties of various classes of semigroups (commutative, left/right-regular bands, semilattices, etc.).

Les omega-catégories faibles, comme toutes les structures supérieures, sont délicates a définir et a manipuler. La raison est qu'elles ont de la structure dans toutes les dimensions, et que cette structure est cohérente: pour chaque dimension, les bonnes propriétés vérifiées par la structure dans cette dimension sont encodées par des éléments de dimension supérieure. La conséquence est qu'au fur et à mesure que l'on monte en dimension, les éléments présents deviennent de plus en plus riches et complexes a décrire. Ainsi, les définitions possibles de ces structures s'appuient sur des schémas d'axiomes, permettant de générer l'infinité d'opérations et de cohérences en toute dimensions, et ces schémas d'axiomes sont eux-mêmes encodés dans des structures algébriques adéquates, comme une opérade globulaire (définition due a Batanin et Leinster) ou une catégorie avec certaines colimites (définition due a Grothendieck et Maltsiniotis). Plus récemment, Finster et Mimram ont proposé une définition des omega-catégories faibles en encodant ces schémas d'axiomes dans une théorie des types, CaTT. Dans cet exposé, je vais présenter la theorie CaTT et m'appuyer sur cette formulation pour présenter formellement les omega-categories faibles. Je vais ensuite faire une démonstration d'un assistant de preuve pour les oméga-categories faibles que j'ai implementé en m'appuyant sur cette théorie des types et discuter des possibilités de cet outil, ainsi que des améliorations que j'y ai apportées. Je vais finalement esquisser une comparaison entre CaTT et la définition de Grothendieck-Maltsiniotis des omega-catégories faibles.

We introduce probabilistic analysis techniques for the testing of programs based on concurrent models. During this talk we study the notion of process synchronization from the point of view of combinatorics. As a first step, we address the quantitative problem of counting the number of executions of simple processes interacting with synchronization barriers. We elaborate a systematic decomposition of processes that produces a symbolic integral formula to solve the problem. Based on this procedure, we develop a generic algorithm to generate process executions uniformly at random. For some interesting sub-classes of processes we propose very efficient counting and random sampling algorithms. All these algorithms have one important characteristic in common: they work on the control graph of processes and thus do not require the explicit construction of the state-space. By consequence, we thus completely avoid the classical combinatorial explosion induced by such processes.

We provide an overview of the techniques developed and results obtained in the field of Implicit Computational Complexity, which aims at providing machine-independent or PL-based characterizations of complexity classes. After discussing some related results on “infinite data” (streams, real numbers, functions, …), we present a new tractable characterization of the class of Basic Feasible Functionals (BFF), known to be the class of second order functions computable in polynomial time. The corresponding programs consist of simply-typed terms that can call strongly normalizing imperative procedures following a tier-based type discipline.

We propose a systematic approach to approximate the behavior of models of polymers with synthesis and degradation. Our technique consists in discovering time-dependent lower and upper bounds for the concentration of some quantities of interest. These bounds are obtained by approximating the state of the system by a hyper-box,. The evolution of the position of each hyper-face is defined by the means of differential equations which are obtained by pessimistically bounding the derivative with respect to the corresponding coordinate on this hyper-face.

The over-approximation of each derivative relies on symbolic reasoning. We use Kappa to describe our models. Kappa is a site-graph rewriting languages which is popular to describe protein-protein interaction networks. The main ingredients of Kappa, graph patterns, can be interpreted in two ways. Intensionally by the means of embeddings between graphs, or extensionally as the (potentially infinite) multi-sets of the complete graphs they occur in. This second interpretation leads to the definition of positive series of concentration of species. Interestingly, it can be proven that some universal constructions between graphs induce generic methods to prove the well-posedness of some numerical series, and some equality and inequality among them, hence providing a convenient tool-kit for symbolic reasoning