Normalization by realizability also computes
- December 2, 2014
- Last updated on 2014/12/02
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
