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 λ-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. 1 General setting

• Type: Conference
• Year: 2007
• Where: TPHOL
• Authors: François Garillot, Benjamin Werner
• Keywords: Artificial Intelligence, Decompilation Function, Formal Treatment, TPHOL 2007, Type Theory