Logics/document/CTT.tex

1 \chapter{Constructive Type Theory}
2 \index{Constructive Type Theory|(}
6 Martin-L\"of's Constructive Type Theory \cite{martinlof84,nordstrom90} can
13 Type Theory.  Nuprl is an elaborate implementation~\cite{constable86}.
17 Isabelle's original formulation of Type Theory was a kind of sequent
28 The theory~\thydx{CTT} implements Constructive Type Theory, using
45 standard Type Theory.  Contexts, which are typical of many modern type
57   \cdx{Type}    & $t \to prop$          & judgement form \\
87 CTT supports all of Type Theory apart from list types, well-ordering types,
96 CTT uses the 1982 version of Type Theory, with extensional equality.  The
394 The rules obey the following naming conventions.  Type formation rules have
405 judgement \cdx{Reduce} does not belong to Type Theory proper; it has
451 versions of Type Theory use intensional equality~\cite{nordstrom90}.
470 The Type Theory tactics provide rewriting, type inference, and logical
471 reasoning.  Many proof procedures work by repeatedly resolving certain Type
586 intuitionistic logic.  However, Constructive Type Theory is not just another
591 represents a proposition, and Type Theory assumptions declare variables.
594 can be deleted safely.  In Type Theory, $+$-elimination with the assumption
718 remainder and quotient, respectively.  Since Type Theory has only primitive
753 Type inference involves proving a goal of the form $a\in\Var{A}$, where $a$
764 Since the term is a Constructive Type Theory $\lambda$-abstraction (not to
827 Logical reasoning in Type Theory involves proving a goal of the form
838 distributive law of Type Theory:
1070 In principle, the Axiom of Choice is simple to derive in Constructive Type
1217 Routine type-checking goals proliferate in Constructive Type Theory, but
1257 \index{Constructive Type Theory|)}