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
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
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
472 Theory rules against a proof state.  CTT defines lists --- each with
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
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:
1071 Theory.  The following definitions work:
1217 Routine type-checking goals proliferate in Constructive Type Theory, but
1257 \index{Constructive Type Theory|)}