Realizability Models for Type Theories
Bernhard Reus · Electronic Notes in Theoretical Computer Science · 1999
This tutorial aims at giving an account on the realizability models for several constructive type theories. These range from simply typed λ-calculus over second-order polymorphic λ-calculus to the Calculus of Constructions as an example of dependent type theory. The models are made from partial equivalence relations (pers) and realizability sets over an arbitrary partial combinatory algebra. Realizability semantics does not only provide intuitive models but can also be used for proving independence results of type theories. Finally, by considering complete extensional pers, an approach to bridge the gap from type theory to constructive domain theory is discussed.