Talk at the Gallium seminar: Proof theoretic results concerning sum types and control operators

January 23, 2015

On March 9, I am giving a talk at the Gallium seminar. Abstract: In this talk, I will present some recent results from Proof Theory that might also be interesting to Programming Languages Theory. First, I will present work on isomorphisms of types in presence of sums, as well as the implications for canonicity of eta-long normal forms of lambda calculus with sums. Second, I will show how one can use a normalization-by-evaluation proof (written in CPS style) to compile away control operators from System T; this could be used as a compiler technique for a side-effect-free fragment of a program.

http://gallium.inria.fr/seminar.html

Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net