doc-src/Logics/CTT.tex
changeset 7159 b009afd1ace5
parent 6170 9a59cf8ae9b5
child 9695 ec7d7f877712
equal deleted inserted replaced
7158:ac93579530ea 7159:b009afd1ace5
     1 %% $Id$
     1 %% $Id$
     2 \chapter{Constructive Type Theory}
     2 \chapter{Constructive Type Theory}
     3 \index{Constructive Type Theory|(}
     3 \index{Constructive Type Theory|(}
       
     4 
       
     5 \underscoreoff %this file contains _ in rule names
     4 
     6 
     5 Martin-L\"of's Constructive Type Theory \cite{martinlof84,nordstrom90} can
     7 Martin-L\"of's Constructive Type Theory \cite{martinlof84,nordstrom90} can
     6 be viewed at many different levels.  It is a formal system that embodies
     8 be viewed at many different levels.  It is a formal system that embodies
     7 the principles of intuitionistic mathematics; it embodies the
     9 the principles of intuitionistic mathematics; it embodies the
     8 interpretation of propositions as types; it is a vehicle for deriving
    10 interpretation of propositions as types; it is a vehicle for deriving