Proof assistant kernels are a natural target for program certification: they are small, critical, and well-specified. Still, despite the maturity of the field of software certification, we are yet to see a certified Agda, Coq or Lean. In this talk, I will try and explain why this is not such an easy task, and present two complementary projects going in that direction. The first, MetaCoq, is a large scale project, broadly aiming at giving tools to manipulate Coq terms and derivations inside of Coq, in particular developing an important body of formalized proofs around Coq's typing. The second is a more recent endeavour, aimed at tackling the mother of all properties: normalisation.

The game comonads research programme, started by Samson Abramsky and Anuj Dawar in 2017, provides categorical accounts of key constructions in finite model theory, and has led to an axiomatic approach to various notions of logical resources central to this field.

I will outline some preliminary ideas on how to bring the tools of homotopy theory to the research area of game comonads, with the aim of tackling open questions concerning e.g. expressive completeness and preservation results.

Joint session with the CHOCOLA seminar. See details at:

https://chocola.ens-lyon.fr/events/meeting-2023-11-16/

Certain properties of (type) dependencies in typed programming languages can be established syntactically by observing non-violation, shortcutting the need of a manual proof. Examples of such properties are variance, irrelevance, parametricity, or causality as in guarded type theory. A type system where function types are annotated with a *modality* expressing the function's behaviour, can account for this syntactic check as part of type-checking. From the need to type basic function operations, we find that these modalities should have the structure of an ordered monoid, or more generally they can be the morphisms of a 2-category whose objects are called *modes*. The purpose of multi[mode/modal] type theory (MTT) is to provide a type system, parametrized by a 2-category called the *mode theory* which abstractly achieves this result.

After introducing MTT and its models, depending on the timing and the interests and background of the audience, we can either look at questions arising during the implementation of MTT, or at applications. Some applications that I have worked on, or am working on, are Degrees of Relatedness (for parametricity & irrelevance), naturality type theory (naturality & variance), and the modal transpension system (for internalizing aspects of presheaf models). J. Ceulemans' Sikkel library for Agda explores how MTT can help to use the many extensions of type theory found in the literature *locally and modularly*.

L'Internet est un réseau consistant de plusieurs dizaines de milliards de nœuds. Le *routage* est le problème d'acheminer un paquet à travers un réseau. Le paradigme de routage utilisé dans l'Internet s'appelle le *routage next-hop*.

Dans cet exposé, je ferai une introduction au routage next-hop, puis je décrirai comment il est traditionnellement réalisé dans l'Internet. Je décrirai les faiblesses des techniques traditionnelles de routage, et je montrerai comment le protocole de routage Babel vise à les contourner.

Titles and abstracts available at: https://chocola.ens-lyon.fr/events/meeting-2023-09-28/

Metaprogramming is the art of writing programs that produce or manipulate other programs. This opens the possibility to eliminate boilerplate code and exploit domain-specific knowledge to build high-performance programs. While this widely used concept is almost as old as programming itself, it has been surprisingly challenging to extend to logical frameworks and type-theory in general.

In this talk, I present a layered modal type theory that provides a logical foundation to meta-programming with intensional code analysis. At its core (layer 0), has a pure (simply-typed) calculus with no modality. Layer 1 is obtained by extending the core with one layer of contextual box types which describes open code at layer 0 and supports pattern matching on open code from layer 0. Although both layers fundamentally share the same language and the same typing judgment, we only allow computation at layer 1. As a consequence, layer 0 accurately captures the syntactic representation of code in contrast to the computational behaviors at layer 1. The system is justified by normalization by evaluation (NbE) using a presheaf model. The normalization algorithm extracted from the model is sound and complete and is implemented in Agda.

We see this work as a stepping stone towards developing a dependent type theory that supports intensional code analysis in meta-programming.

This is joint work with Jason Z. Hu.

Barendregt's book “The Lambda Calculus, its syntax and semantics” (1981/84) has become a `classic' in Theoretical Computer Science because it presents the state of the art in lambda calculus in a comprehensive way, and proposes a number of open problems and conjectures. In 2022, Barendregt and Manzonetto published a `sequel' of this book, presenting the solutions of several of these problems, and more. In this talk, we will present a selection of these problems and the key ingredients that were employed to solve them.

Topology-based geometric modeling deals with the representation of nD objects, which splits the topological description, i.e., the representation of the objects' topological cells (vertices, edges, faces, volumes, …), and the geometric information, i.e., the addition of data to the topological cells. We study the combinatorial models of generalized and oriented maps represented as attributed typed graphs subject to consistency conditions. This representation allows the study of modeling operations as graph rewriting rules. The motivation is twofold. First, we study the preservation of the model consistency through syntactic conditions statically checked on the rules. Second, we extend rules into rule schemes to abstract over the underlying topology. This formalization of modeling operations also offers guidelines for inferring operations from a representative example consisting of an initial and a target object. The inference mechanism is implemented in Jerboa, a platform for designing geometric modelers exploiting graph transformation rules.

Milner's work on functions as processes shows how the evaluation strategies of the lambda-calculus can be faithfully mimicked in the pi-calculus, allowing a dynamic representation of functional programs. Milner namely studies the call-by-name and call-by-value evaluation strategies, and raises the problem of full abstraction for these encodings, i.e., what are the equivalences induced by these encodings. The theory of call-by-name is well-studied and understood, and the problem of full abstraction for call-by-name was solved shortly after. On the other hand, the theory of call-by-value on open terms is complex, and we present the solution of the full abstraction problem for call-by-value, which was left open until quite recently.

Algebraic operations, as defined by Plotkin and Power, are well-studied and powerful tools to provide denotational semantics for computational lambda-calculus and it is especially useful in design for abstraction of effectful computations, allowing a high degree of modularity by separating effect signatures from their interpretations. The practical counterpart of this is obtained by the use of handlers, a popular tool in functional programming that can actually provide concrete implementations of effect signatures while preserving modularity.

In this talk, I will present a joint work with Ugo Dal Lago and Francesco Gavazzo on how algebraic operations, and handlers, can support decision-making abstractions in functional programs: a user can invoke an operation to resolve choices without implementing the underlying selection mechanism, and can give feedback by way of rewards. We differ from some recently proposed approach to the problem based on the selection monad, by Abadi and Plotkin, as we express the underlying selection mechanism with efficient algorithms implemented by a set of handlers. I will first introduce algebraic effects and handlers, then present the selection monad approach for choices, and our approach, based on stateful computations (or equivalently comodels). Both the theoretical and practical aspects will be examined, and I will show the practical efficiency of our approach compared to the selection monad. Finally, I will focus on how our work can actually be implemented in a modular way on a concrete language with handlers and how we can use expressive type systems to obtain safety properties, especially ensuring a high-degree of modularity and a sound usage of algebraic operations.

Program execution rarely happens in isolation. Indeed, during its evaluation a program may modify the memory of the machine, interact with external processes, change the flow of the computation, etc. All these phenomena are known as computational effects, and they can be informally described as those side effects happening during the evaluation process of the program. Computational effects are of paramount importance to understand program behaviour, and indeed they are one of the main research topics in programming language semantics since the very birth of the discipline. Starting with the seminal work by Eugenio Moggi, computational effects have been successfully understood relying on the language of algebra and category theory, with notions such as monad, algebraic (and Lawvere) theory, and distributive law being nowadays well-accepted idioms in the programming language community. Although the categorical perspective on computational effects has been particularly effective to model the denotational semantics of effectful programs it does not work so well when it comes to accounting for their operational behaviour. In this talk, I will introduce the theory of computational effects by first reviewing the categorical approach to effectful programs, focusing in particular on Plotkin and Power's theory of algebraic effects, and then moving to computational effects in (some subfields of) operational reasoning. In particular, I will give evidence that by extending the aforementioned categorical notions from a categorical (functional) to an allegorical (relational) setting, it is possible to obtain an elegant operational theory of computational effects having the same level of generality as its denotational counterpart. To maintain the talk as accessible as possible, I will give a first introductory part on computational effects and then move to the more technical relational development. The latter will consist of a general high-level outline of the results achieved in the context of operational reasoning and of a more in-depth case study.

In this talk, we introduce two complete equational theories: one for linear optical circuits and one for quantum circuits. More precisely, in both cases we introduce a set of circuit equations that we prove to be sound and complete: two circuits represent the same quantum evolution if and only if they can be transformed one into the other using the equations.

We shall first present our proposed equational theory for linear optical circuits. We shall then discuss how the semantics of both kind of circuits differ, and how to relate them using controlled-gates. The discussion will drive is to the completeness result for quantum circuits, based on the one for linear optical circuits.

ML modules are offer large-scale notions of composition and modularity. Provided as an additional layer on top of the core language, they have proven both vital to the working OCaml and SML programmers, and inspiring to other use-cases and languages. Unfortunately, their meta-theory remains difficult to comprehend, and more recent extensions (abstract signatures, module aliases) lack a complete formalization. Building on a previous translation from ML modules to Fω, we propose a new comprehensive description of a significant subset of OCaml modules, including both applicative and generative functors and the proposed feature of transparent ascription. By exploring the translations both to and from Fω, we provide a complete description of the signature avoidance issue, as well as insights on the limitations and benefits of the path-based approach of OCaml type-sharing.

(Joint work with Almudena Colacito, Nikolaos Galatos, and Simon Santschi)

This talk will be about deciding equations in various classes of ordered groups and ordered monoids, and how this relates to deciding if there exist orders on free groups and monoids satisfying finitely many inequalities.

Removing the inverse operation from any lattice-ordered group (l-group) yields a distributive lattice-ordered monoid (l-monoid), but not every distributive l-monoid admits a group structure. Indeed, every distributive l-monoid is a (possibly finite) pointwise-ordered monoid of order-preserving maps on a chain, whereas every l-group is a pointwise-ordered group of order-preserving permutations on a chain and must be either trivial or infinite.

We will see that the equational theory of distributive l-monoids is decidable and coincides with the equational theory of l-groups without inverses, and hence, by eliminating inverses, that the equational theory of l-groups is also decidable. This contrasts with the fact that there are inverse-free equations that are satisfied by all totally ordered abelian groups but not all totally ordered commutative monoids, and the decidability of the equational theory of the latter is open.

Ehrhard and Regnier’s Taylor expansion of λ-terms has been broadly used as an approximation theory for several variants of the λ-calculus. Many results arise from a Commutation theorem relating the normal form of the Taylor expansion of a term to its Böhm tree. We extend this framework to the (001-)infinitary λ-calculus, where terms and reductions may be infinite, and where the normal forms are precisely the Böhm trees. This enables us to give a unified presentation of the Commutation theorem, thanks to the simulation of the infinitary reduction by the (finitary, confluent and terminating) reduction of the Taylor expansion. Finally we deduce new, simple proofs of confluence and genericity for the infinitary λ-calculus, as well as approximation-based characterisations of head- and β-reductions.

Corresponding paper (submitted to LMCS): https://arxiv.org/abs/2211.05608. This is joint work with my supervisor Lionel Vaux Auclair (I2M, AMU).