Groupe de travail

Équipe thématique Preuves et programmes

Jour, heure et lieu

Le mercredi à 14h, salle 1007


Pour recevoir les annonces, s'abonner ici.

Prochaines séances

Théorie des types et réalisabilité
mercredi 20 décembre 2017, 14h00, Salle 1007
Ludovic Patey () Sur les degrés de Weihrauch

Séances précédentes

Théorie des types et réalisabilité
mercredi 06 décembre 2017, 14h00, Salle 1007
Francesco A. Genco (IRIF - TU Wien) Typing Parallelism and communication through hypersequents

We present a Curry–Howard correspondence for Gödel logic based on a simple natural deduction reformulating the hypersequent calculus for this logic. The resulting system extends simply typed λ-calculus by a symmetric higher-order communication mechanism between parallel processes. We discuss a normalisation procedure and several features of the parallel λ-calculus. Following A. Avron's 1991 thesis on the connection between hypersequents and parallelism, we also discuss the generalisation of the employed techniques for other intermediate logics.

Théorie des types et réalisabilité
mercredi 29 novembre 2017, 14h00, Salle 1007
Guilhem Jaber (ENS Lyon) A Trace Semantics for System F Parametric Polymorphism

In this talk, we present a trace model for System F that captures Strachey parametric polymorphism. The model is built using operational nominal game semantics and enforces parametricity by using names. This model is used here to prove a conjecture of Abadi, Cardelli, Curien and Plotkin which states that Strachey equivalence implies Reynolds equivalence (i.e. relational parametricity) in System F.

Théorie des types et réalisabilité
jeudi 16 mars 2017, 14h00, Salle 1007
Pierre-Marie Pédrot () An Effectful Way to Eliminate Addiction to Dependence

We define a syntactic monadic translation of type theory, called the weaning translation, that allows for a large range of effects in dependent type theory, such as exceptions, non-termination, non-determinism or writing operation. Through the light of a call-by-push-value decomposition, we explain why the traditional approach fails with type dependency and justify our approach. Crucially, the construction requires that the universe of algebras of the monad forms itself an algebra. The weaning translation applies to a version of the Calculus of Inductive Constructions with a restricted version of dependent elimination, dubbed Baclofen Type Theory, which we conjecture is the proper generic way to mix effects and dependence. This provides the first effectful version of CIC, which can be implemented as a Coq plugin.