Sjödin, Gunnar and Löfwall, Clas (1991) Strong normalizability in Martin-Löf's Type Theory. [SICS Report]
In this paper we prove that any subexpression of a correct judgement in Martin-Löf's Type Theory is strongly normalizable. We use the well-established technique with a ``computability predicate''. The logic used in the proof is classical set theory.
|Item Type:||SICS Report|
|Deposited By:||Vicki Carleson|
|Deposited On:||23 Oct 2009|
|Last Modified:||18 Nov 2009 16:00|
Repository Staff Only: item control page