## Type theory and realisability

#### Day, hour and place

Wednesday at 2pm, room 1007

#### Contact(s)

#### Future talks

Théorie des types et réalisabilité

mercredi 20 décembre 2017, 14h00, Salle 1007

**Ludovic Patey** () *Sur les degrés de Weihrauch*

#### Past talks

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.