Programme

Vous pouvez proposer vos exposés jusqu’au 27 Octobre.

Orateurs invités

Valentin Blot (Paris-Sud), Polymorphism vs. Bar Recursion: towards a new termination proof for System F

Spector defined bar recursion in 1962 to extend Gödel’s Dialectica interpretation of arithmetic to full mathematical analysis, that is, arithmetic with the axiom scheme of comprehension. In the early 70’s, Girard and Reynolds discovered another unrelated interpretation of second-order arithmetic: polymorphic lambda-calculus. While the logical equivalence between analysis and second-order arithmetic has always been clear, the computational counterpart did not receive much attention. My talk gives a first step towards filling this gap by presenting an interpretation of System F into System T augmented with bar recursion. While both languages are total, their termination proofs are very different: the only known proofs of termination of System F rely on the impredicative notion of reducibility candidates (or saturated sets), while termination of bar recursion is usually proven with the axiom of dependent choice. My goal is to combine the interpretation of System F into System T + bar recursion with a proof of termination of bar recursion, so as to obtain a new proof of termination for System F that does not rely on the impredicative notion of reducibility candidates.

Amina Doumane (ENS Lyon), Completeness of mu-calculi and the mystery of circular proofs

Paul-André Melliès (IRIF), Automates à parité d’ordre supérieur

Dans cet exposé, j’expliquerai comment définir une notion d’automate à parité capable de reconnaitre (ou de rejeter) un lambda-terme simplement typé avec points fixes. La notion d’automate à parité que je formulerai étend grandement le domaine d’application traditionnel du model-checking d’ordre supérieur. Elle éclaire aussi un lien profond et inédit entre théorie des automates et modèles relationnels de la logique linéaire. Du point de vue technique, la preuve de décidabilité que je présenterai repose sur une combinaison d’idées issues de la sémantique dénotationnelle et de la réécriture infinitaire. Ce travail marque une étape de clarification dans un programme de recherche lancé aux côtés de Charles Grellois (LIF) et en affinité élective avec les travaux de Sylvain Salvati (CRIStAL) et Igor Walukiewicz (LaBRI).

Pierre-Marie Pédrot (MPI-SWS), Taming effects in a dependent world

In the traditional view of the Curry-Howard isomorphism, Martin-Löf type theory is a total functional programming language, or equivalently a hardcore intuitionistic theory. Although it seemed close to impossible to come up with a way to alter this property by adding effects to it, we recently challenged this belief. By using the so-called syntactic model approach, which consists in compiling a type theory into another one through crazily dependent program transformations, we showed that it was actually possible to extend MLTT with impure constructions. There is an implicit tension between the features of MLTT though, and a few assumptions need to be relaxed. Intuitively, in an effectful world, there is a type-theoretical ‘triangle of fire’ and one is forced to pick only two properties out of the three following ones: unrestricted conversion (i.e. call-by-name theory), logical consistency, and dependent elimination. Led by our bottomless faith in Curry-Howard and riding our flawless Coq destrier, we will jump into the chasm to explore the parallel universes where one of the two latter conditions are weakened. Along our journey, we will discover that lies can bring truth, that value restriction has an evil twin, and that semantics of MLTT is really bad for your mental health.

Les commentaires sont clos.