In summer 2015, I investigated in Coq the function G introduced by Hofstadter in his famous “Gödel, Escher, Bach” book:

$G(n) = n - G(G(n-1))$ for $n>0$ and $G(O) = 0$

This involves a related infinite tree, where Fibonacci numbers will show up (what else ?). I'll also talk about Zeckendorf decomposition. The left/right flipped variant of this G tree has also been studied here, following Hofstadter's ``problem for the curious reader''. This lead me to a (Coq) proof of an algebraic formulation for the flipped function.

In this patchwork talk, I will present several aspects of my recent work that put (or will put) Coq as a functional programming language of choice for the discriminating mathacker (contraction of mathematician and hacker).

Interfaces for computational effects provide a mathematically structured basis for organizing code: monads, arrows and applicative functors have became a fundamental part of the Haskell programmer's toolbox. In this talk we revisit these interfaces, show how category theory tell us what they have in common, and how we can relate them.

Since their inception in 1997 by Baez and Dolan, opetopes have been redefined and studied in a few different ways. However, they always appear as highly inductive, and thus extremely tricky to manipulate. During this talk, i will give an informal definition of opetopes, introduce some tools and notations, and present a syntax for opetopes developed in a joint work with Pierre-Louis Curien and Samuel Mimram.

Je parlerais de comment mélanger les travaux sur l'unification, le filtrage dépendant, la réification et la compilation certifiée pour obtenir un noyau de Coq “du futur” certifié. Je ferai essentiellement un panorama de mes travaux passés et futur autour de Coq et les outils/formalisations associées: les univers, UniCoq, TemplateCoq, CertiCoq, Equations et CoqHoTT en montrant la construction par étage d'une chaîne de développement certifiée de programmes ou de mathématique, et les problèmes ouverts associés.

I will discuss a recognition principle for left exact modalities in homotopy type theory and explain how it relates to the problem of understanding subtopoi of $\infty$-topoi. This theory generalizes the classical theory of Lawvere-Tieney topologies to the case of higher topoi. I will also describe some new phenomena which arise in the higher dimensional case.

Le produit smash est une opération très utilisée en topologie algébrique, et qui peut être définie en théorie homotopique des types par un certain type inductif supérieur. Mais quand on essaye de démontrer qu’il satisfait certaines propriétés (commutativité, associativité), cela devient vite très technique et essentiellement impossible à faire à la main. Dans cet exposé, je vais expliquer les problèmes qui se présentent et la façon dont je compte les résoudre: en écrivant un programme qui génère automatiquement une démonstration formelle du résultat souhaité (en Agda).