réunion plénière année 4 du défi LiberAbaci

Lieu de la réunion: salles 3052 et 3071, Irif, Paris

Nouvelle : Les financements autour du projet LiberAbaci ont finalement été débloqués : on pourra donc faire cette réunion en présentiel. Cependant, au vu des délais très court, nous comprenons si tout le monde ne puisse pas participer et nous ferons en sorte que l'on puisse y participer en visio en plus du présentiel.

La salle 3052 est réservée tout du long, sauf entre 11h et 12h où nous serons salle 3071.

14 avril, 2026

• 9:30–9:45 Cyril Cohen et Martin Bodin, objectifs de la dernière année du défi
• 9:45–10:10 Frédéric Tran Minh, Sébastien Lahaye Présentation Yalep
• 10:10–10:35 Cécile Marcon
• 10:35–11:00 Julien Puydt Typage cadré

• 11:00–12:00 Discussions en petits groupes, salle 3071

• 12:00–13:30 Pause repas

• 13:30–13:55 présentation Malinca
• 13:55–14:20 Arthur Charguéraud, typage overloading, dernier épisode !
• 14:20–14:55 Emmanuel Beffara, Nathan Coquerel, Un outil pour l'enseignement de la preuve associant les registres textuel et visuel

• 14:55–15:30 Pause café

• 15:30–15:55 Yves Bertot, Travaux sur l'utilisation d'un seul type dans la présentation formelle des mathématiques
• 15:55–16:20 Thiago Felicissimo, À propos d'une extension de la théorie des types observationnelle avec des prédicats d'accessibilité

• 16:20–17:00 Discussions sur la suite du défi

Résumés

Arthur Charguéraud, typage overloading, dernier épisode !

Thiago Felicissimo, À propos d'une extension de la théorie des types observationnelle avec des prédicats d'accessibilité

A universe of propositions equipped with definitional proof irrelevance constitutes a convenient medium to express properties and proofs in type-theoretic proof assistants such as Lean, Rocq, and Agda. However, allowing accessibility predicates—used to establish semantic termination arguments—to inhabit such a universe yields undecidable typechecking, hampering the predictability and foundational bases of a proof assistant. To effectively reconcile definitional proof irrelevance and accessibility predicates with both theoretical foundations and practicality in mind, we describe a type theory that extends the Calculus of Inductive Constructions featuring observational equality in a universe of strict propositions, and two variants for handling the elimination principle of accessibility predicates: one variant safeguards decidability by sticking to propositional unfolding, and the other variant favors flexibility with definitional unfolding, at the expense of a potentially diverging typechecking procedure. Crucially, the metatheory of this dual approach establishes that any proof term constructed in the definitional variant of the theory can be soundly embedded into the propositional variant, while preserving the decidability of the latter. Moreover, we prove the two variants to be consistent and to satisfy forms of canonicity, ensuring that programs can indeed be properly evaluated. We present an implementation in Rocq and compare it with existing approaches. Overall, this work introduces an effective technique that informs the design of proof assistants with strict propositions, enabling local computation with accessibility predicates without compromising the ambient type theory.

Yves Bertot, Travaux sur l'utilisation d'un seul type dans la présentation formelle des mathématiques

Emmanuel Beffara, Nathan Coquerel, L'état actuel d'un projet d'outil pour l'enseignement de la preuve, basé sur l'utilisation d'un langage naturel contrôlé et cherchant à permettre l'association de registres textuel et visuel

Informations de connection en ligne

Lien de la réunion

https://webinaire.numerique.gouv.fr/meeting/signin/invite/74153/creator/23124/hash/39fff4e5e1b1e8d4cf26249cfec1b5b356839ceb