realizability

Discussion of the connection between normalization and logical consistency.  One approach is to prove normalization and type preservation, to show (in proof-theoretic terms) that all detours can be eliminated from proofs (this is normalization) and that the resulting proof still proves the same theorem (this is type preservation).  I mention an alternative I use for Cedille, which is to use a realizability semantics (often used for normalization proofs) directly to prove consistency.

Curry-style typing and realizability make it sensible to allow a top type to type every term, even non-normalizing ones.

Types are specifications whose semantics is explained in terms of computation, which is thus conceptually prior.  Realizability is a way of explaining the semantics of types.