Friday 12 February 2016, 10:30: Contextual types for multi-staged programming, Matthias Puech (Université Paris Diderot).

Programming languages that allow us to manipulate code as data pose a notorious challenge to type system designers. In particular, multi-stage programming, as found in MetaOcaml for instance, has been known for a long time to be related to modal logics, but the first attempts, by Davies and Pfenning, at establishing a formal correspondence showed important flaws.

We propose contextual type theory with first-class environments as a foundational typing discipline for multi-stage functional programming. It strictly subsumes previous proposals while being based on a Curry-Howard correspondence with a finer-grained modal logic: contextual logic. In particular, we show a conservative embedding of Taha and Nielsen’s environment classifiers into it.

After a quick overview on multi-stage programming and why it is difficult to design type systems for it, we will introduce contextual types and present the embedding. Finally, we will hint at the consequences of this result, both on the logic side--what it implies for the underlying modal logic--and for programming--how it can help simplifying the process of normalization.

This is joint work with Brigitte Pientka.