Journées $\pi r^2$ 2018 à Fontainebleau 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).