@inproceedings{41a87e00070b41aeabc2b7be589e96c5,
title = "Simple types in type theory: Deep and shallow encodings",
abstract = "We present a formal treatment of normalization by evaluation in type theory. The involved semantics of simply-typed A-calculus is exactly the simply typed fragment of the type theory. This means we have constructed and proved correct a decompilation function which recovers the syntax of a program, provided it belongs to the simply typed fragment. The development runs and is checked in Coq. Possible applications include the formal treatment of languages with binders.",
author = "Fran{\c c}ois Garillot and Benjamin Werner",
year = "2007",
month = jan,
day = "1",
doi = "10.1007/978-3-540-74591-4\_27",
language = "English",
isbn = "9783540745907",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "368--382",
booktitle = "Theorem Proving in Higher Order Logics - 20th International Conference, TPHOLs 2007, Proceedings",
note = "20th International Conference on Theorem Proving in Higher-Order Logics, TPHOLs 2007 ; Conference date: 10-09-2007 Through 13-09-2007",
}