I will first give a quick overview of my research interests : automated and interactive proof in geometry, using proof assistant for teaching, then I will focus on recent joint work with Predrag Janičić about the use constraint solving for automatic theorem proving. One of the features of the implemented prover Larus is that it can generate human understandable proofs in natural language and also machine-verifiable proofs for the interactive prover Coq.

The somehow pedantic title of this talk hides a simple and very old (yet not fully explored for a long time) idea: The dynamics of β-reduction is intrinsically coinductive. The goal of my PhD thesis was to take this idea seriously in the setting of the linear approximation of the λ-calculus, i.e. to reformulate the Taylor expansion of λ-terms in an infinitary setting. Doing this allows to reorganise many results, including the good old continuous approximation based on approximation orders.
I will conclude this tentative autobiography of a very short scientific life with a few words about other topics I have been, am currently, or would like to be working on -- all gravitating around this idea of infinitary dynamics.

Calculus with disjoint intersection types supports a symmetric merge operator which generalizes record concatenation. Equipped with distributive subtyping, such a type discipline provides a foundation for Compositional Programming, a new modular style of statically typed programming that features dynamic inheritance, in which solutions to the expression problem arise naturally. In this talk, I will briefly overview the core calculus of disjoint intersection types and explore its design space. During my postdoc, I am studying the module system of Elixir, a dynamic functional programming language. I aim to incorporate it into the recently developed static type system of Elixir—a polymorphic type system with set-theoretic types and semantic subtyping. Semantic subtyping interprets types as sets of values and provides a different understanding of intersection types. My current goal is to explore how to encode the first-class modules in Elixir with existential types and to establish a set-theoretic interpretation for existential types.

TBA

I will give a brief overview of the lines of work I’m currently involved with, that all more or less connect to the mechanisation of (constructive) reverse mathematics in the Coq proof assistant. I’ll focus on the logical analysis of theorems concerning first-order logic and computability theory but will also describe how this analysis motivates studying particular models of intuitionistic higher-order logic and constructive type theory.