Mardi 10 avril

10h – 11h · Yves Guiraud · Théorie de Squier et application aux monoïdes d'Artin

11h15 – 12h15 · Pierre Letouzey · Hofstadter’s problem for curious readers

Déjeuner

14h15 – 15h15 · Yann Régis-Gianas · Differences and Infinity in Purely Functional Programming

15h30 – 16h30 · Exequiel Rivas · A few comments on interfaces for computational effects

Pause-café

17h – 18h · Hugo Herbelin · Vers une convergence de la syntaxe de la théorie des types et de la syntaxe des $\omega$-groupoïdes

20h – Dîner au Smile

Mercredi 11 avril

8h – Petit déjeuner

9h – 9h45 · Hugo Herbelin · Polarisation, traductions et théorie des types

10h – 10h45 · Cédric Ho Thanh · A Syntactical Definition of Opetopes

Pause-café

11h15 – 12h15 · Matthieu Sozeau · Un environnement pour la programmation avec types dépendants, IIème reprise

Déjeuner

14h15 – 15h15 · Eric Finster · Left Exact Modalities in Type Theory

15h30 – 16h30 · Guillaume Brunerie · Démonstrations générées par ordinateur pour le produit smash

Pause-café

17h – 18h · Alexis Saurin · Un petit tour au pays des preuves circulaires

Résumés

Pierre : Hofstadter’s problem for curious readers

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.

Yann : Differences and Infinity in Purely Functional Programming

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).

Exequiel : A few comments on interfaces for computational effects

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.

Cédric : A Syntactical Definition of Opetopes

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.

Matthieu : Un environnement pour la programmation avec types dépendants, IIème reprise

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.

Eric : Left Exact Modalities in Type Theory

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.

Guillaume : Démonstrations générées par ordinateur pour le produit smash

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).