Vous pouvez vous abonner à nos annonces de séminaires http://gallium.inria.fr/seminaires/ S E M I N A I R E __ / _` _ / / o / ) __) / / / / / /\/| (___/ (_/ (_ (_ / (__/ / | I N R I A - Rocquencourt Amphi Turing du bâtiment 1 Lundi 9 mars, 10h30 ---------- Danko Ilik ---------- INRIA ====================================================== Proof theoretic results concerning sum types (type isomorphism and canonical eta-long normal forms) and control operators ====================================================== 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.