An Adequacy Theorem for Dependent Type Theory

• DOI: 10.1007/s00224-018-9879-9
• Publication Date: 2018-07-28T04:42:02Z
• Authors: Thierry Coquand; Simon Huber
• Keywords: 0102 computer and information sciences; 01 natural sciences

We present a domain model of dependent type theory and use it to prove basic metatheoretic properties. In particular, we prove that two convertible terms have the same Bohm tree. The method used is reminiscent of the use of “inclusive predicates” in domain theory.