Change search
ReferencesLink to record
Permanent link

Direct link
Strong normalizability in Martin-Löf's Type Theory
Number of Authors: 2
1991 (English)Report (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
Kista, Sweden: Swedish Institute of Computer Science , 1991, 1. , 91 p.
SICS Research Report, ISSN 0283-3638 ; R91:09
National Category
Computer and Information Science
URN: urn:nbn:se:ri:diva-14042OAI: diva2:1035325
Available from: 2016-10-13 Created: 2016-10-13

Open Access in DiVA

fulltext(4946 kB)0 downloads
File information
File name FULLTEXT01.pdfFile size 4946 kBChecksum SHA-512
Type fulltextMimetype application/pdf

Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

ReferencesLink to record
Permanent link

Direct link