Gagallium

I share with Pierre Dagand the pleasure of having finished the redaction of a small article on realizability for JFLA 15 (Journées francophones des langages applicatifs). It is a rather simple presentation of the computational content of adequacy proofs, which we hoped to understand better by exhibiting their proof terms as well-typed lambda-terms in a dependently typed meta-language.

http://gallium.inria.fr/~scherer/research/norm_by_rea/dagand-scherer-jfla15.pdf