Applications of type theory

Abstract

The paper discusses the setting of type theory and proposes a uniform framework for disciplines of declarations and types. The framework combines fundamental concepts found in the setting of type theory and supports both its denotational and its constructive view. In the denotational view ε-structures arc introduced as semantic models and in the constructive view the general forms of judgements and rules are given. Finally applications are discussed which build on the ideas of this framework, namely models of untyped λ-calculus which truly solve the equation of reflexive domains, and ε T-logic, a first-order theory of propositions with selfreference and impredicative quantification allowing for intensional models of truth.