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.