"Normalisation by Completeness with Heyting Algebras."

Gaëtan Gilbert, Olivier Hermant (2015)
a service of Schloss Dagstuhl - Leibniz Center for Informatics