~~NOCACHE~~
/* DO NOT EDIT THIS FILE             */

[[seminaires:types:index|Théorie des types et réalisabilité]]\\
Mercredi 20 décembre 2017, 14 heures, Salle 1007\\
**Ludovic Patey** (ICJ, Lyon) //Introduction aux mathématiques à rebours//
<button type="link" size="xs" collapse="b17-3380">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b17-3380" collapsed="true">
<well size="sm">
Les mathématiques à rebours sont un domaine fondationnel qui vise à
trouver les axiomes optimaux pour prouver les théorèmes de la vie de
tous les jours. Elles se placent dans l'arithmétique du second ordre,
avec une théorie de base, RCA, capturant informellement les
"mathématiques calculables". Nous reviendrons sur les justifications
historiques des mathématiques à rebours, présenterons ses principales
observations, ainsi que l'approche moderne des mathématiques à rebours
comme formalisme de classification de phénomènes calculatoires.
</well>
</collapse>


[[seminaires:types:index|Théorie des types et réalisabilité]]\\
Mercredi 6 décembre 2017, 14 heures, Salle 1007\\
**Francesco A. Genco** (IRIF - TU Wien) //Typing Parallelism and communication through hypersequents//
<button type="link" size="xs" collapse="b17-3381">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b17-3381" collapsed="true">
<well size="sm">
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.
</well>
</collapse>


[[seminaires:types:index|Théorie des types et réalisabilité]]\\
Mercredi 29 novembre 2017, 14 heures, Salle 1007\\
**Guilhem Jaber** (ENS Lyon) //A Trace Semantics for System F Parametric Polymorphism//
<button type="link" size="xs" collapse="b17-3382">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b17-3382" collapsed="true">
<well size="sm">
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.
</well>
</collapse>


[[seminaires:types:index|Théorie des types et réalisabilité]]\\
Jeudi 16 mars 2017, 14 heures, Salle 1007\\
**Pierre-Marie Pédrot**  //An Effectful Way to Eliminate Addiction to Dependence//
<button type="link" size="xs" collapse="b17-3383">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b17-3383" collapsed="true">
<well size="sm">
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.
</well>
</collapse>