Simple Types in Type Theory: Deep and Shallow Encodings

DOI10.1007/978-3-540-74591-4_27zbMath1144.68355OpenAlexW1547331954MaRDI QIDQ3523188

Benjamin Werner, François Garillot

Publication date: 2 September 2008

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-74591-4_27

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items (3)

Internal models of system F for decompilation ⋮ Extensible and Efficient Automation Through Reflective Tactics ⋮ N. G. de Bruijn's contribution to the formalization of mathematics

Uses Software

• Coq

This page was built for publication: Simple Types in Type Theory: Deep and Shallow Encodings