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.