Thursday 27 February 2020, 14:00, LSV library: Dependent Type Theory in Polarised Sequent Calculus, Étienne Miquey (Post-doc, Deducteam).

We investigate a minimal setting which unifies type theory (dependently-typed, constructive) and proof theory (polarised, classical), suitable for representing effectful computations in the presence of dependent types and as a vehicle for compilation. We introduce a λ -calculus Ldep which extends both Luo's Extended Calculus of Constructions (ECC) and Girard's polarised classical sequent calculus (LC). We then use it to investigate continuation-passing style translations for dependent type theory from a proof-theoretic point of view. We show how Ldep advantageously factorizes a dependently typed continuation-passing style translation for ECC with control operators. In the pure case, we obtain an unrestricted translation from ECC to itself, thus opening the door to the definition of dependently typed compilation transformation.

This talk is based on joint work (in progress) with Xavier Montillet and Guillaume Munch-Maccagnoni.