SODA

Strong normalizability in Martin-Löf's Type Theory

Sjödin, Gunnar and Löfwall, Clas (1991) Strong normalizability in Martin-Löf's Type Theory. [SICS Report]

[img]Postscript
148Kb
[img]
Preview
PDF
4Mb

Abstract

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
ID Code:2098
Deposited By:Vicki Carleson
Deposited On:23 Oct 2009
Last Modified:18 Nov 2009 16:00

Repository Staff Only: item control page