Rencontre, 26 janvier 2023

Programme

10:30 – 12:00

Yannick Zakowski (INRIA (Lyon))

Invited talk: Monadic Definitional Interpreters as Formal Semantic Models of Computations

Monadic interpreters have been used for a long time as a mean to embed arbitrary computations in purely functional contexts. At its core, the idea is elementary: the object language of interest is implemented as an executable interpreter in the host language, and monads are simply the abstraction used to embed features such as side effects, failure, non-determinism. By building these interpreters on top of the free monad, the approach has offered a comfortable design point notably enabling an extensible syntax, reusable modular components, structural compositional definitions, as well as algebraic reasoning.

The approach has percolated beyond its programming roots: it is also used as a way to formalize the semantics of computational systems, programming languages notably, in proof assistants based on dependently typed theories. In such assistants, the host language is even more restricted: programs are all pure, but also provably terminating. Divergent programs can nonetheless be embedded using for instance the Capretta monad: intuitively, a lazy, infinite (coinductive) tree models the dynamic of the computation.

Interaction trees are a specific implementation, in the Coq proof assistant, of a set of tools realizing this tradition. They provide a coinductive implementation of the iterative free monad, equipped with a set of combinators, allowing notably for general recursion. Each iterator comes with its equational theory established with respect to a notion of weak bisimulation --- i.e. termination sensitive, but ignoring the amount of fuel consumed --- and practical support for equational reasoning. Further effects are implemented into richer monads via a general notion of interpretation, allowing one to introduce the missing algebras required for proper semantic reasoning. Beyond program equivalence, support for arbitrary heterogeneous relational reasoning is provided, typically allowing one to prove a compilation pass correct.

Introduced in 2020, the project has spawned realistic applications --- they are used to model LLVM IR's semantics notably ---, as well as extensions to reduce the necessary boilerplate, or to offer proper support for non-determinism. In this talk, I will attempt to paint an illustrative overview of the core ideas and contributions constitutive of this line of work.

13:50 – 14:50

Zeinab Galal (LIP6, Sorbonne Université)

Invited talk: Bidimensional fixpoint operators

Fixpoint operators are tools to reason on recursive programs and infinite data types obtained by induction (e.g. lists, trees) or coinduction (e.g. streams). They were given a categorical treatment with the notion of categories with fixpoints. An important result by Plotkin and Simpson in this area states that provided some conditions on bifree algebras are satisfied, we obtain the existence of a unique uniform fixpoint operator. This theorem allows to recover the well-known examples of the category Cppo (complete pointed partial orders and continuous functions) in domain theory and the relational model in linear logic. In this talk, I will present a categorification of this result where the 2-dimensional framework allows to study the coherences associated to the reductions of λ-calculi with fixpoints i.e. the equations satisfied by the program computations steps.

15:15 – 16:15

Meven Lennon-Bertrand (Cambridge Univ. (UK))

Invited talk: Bidirectional typing is not just an implementation technique

In 2000, Pierce and Turner introduced a new technique to perform type inference for ML-like languages, whose main idea was to carefully understand the local flow of information in typing rules. This technique, which came to be referred to as bidirectional typing, did not come out of a void: similar ideas had appeared independently in other contexts. In particular, bidirectional typing has been a part of the folklore of dependently typed languages implementers since the dawn of time.

But even in that context where it has a long history, bidirectional typing was missing an understanding that would detach from implementations to focus on the type-theoretic structure. Fortunately, such a type-theoretic bidirectional structure turns out to be a very interesting tool when studying (dependent) type systems.

In my talk, I will try and give some of my understanding of bidirectional typing, how it is both rooted in type-checker implementations but is more than just this, and how it can be used to make the infamously painful meta-theory of dependent type systems a bit less painful.