On the syntax of Martin-Löf's type theories
type: Item
instance of: scholarly article
title: On the syntax of Martin-Löf's type theories
zbMATH Open document ID: 0638.03056
DOI: 10.1016/0304-3975(87)90047-8
author: A. S. Troelstra
published in: Theoretical Computer Science
publication date: 1987-01-01T00:00:00Z
review text: The paper gives a precise syntactical presentation of the arithmetical fragment (without universes and W-operator for the formation of well- founded trees) of Martin-Löf's type theories, both in an intensional and an extensional version. Some elementary proof-theoretic properties are established, such as normalization of terms, the equivalence between several versions, and the dropping of type-statement premises.
Mathematics Subject Classification ID: 03F35
Mathematics Subject Classification ID: 03F50
Mathematics Subject Classification ID: 03F05
zbMATH DE Number: 4039894
zbMATH Keywords: arithmetic fragment of Martin-Löf's type theories
zbMATH Keywords: normalization of terms
describes a project that uses: Automath
describes a project that uses: Nuprl
MaRDI profile type: Publication
full work available at URL: 0304-3975(87)90047-8
OpenAlex ID: W2068339813
cites work: Q3310616
cites work: Semantics for classical AUTOMATH and related systems
cites work: Q3679172
cites work: Q5619069
cites work: Q4099613
cites work: Constructive mathematics and computer programming
cites work: Q3688389
cites work: Q5559220
cites work: Q3768897
cites work: Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
cites work: Q3313859
cites work: Strong normalization for typed terms with surjective pairing
cites work: Q4187337
cites work: Q3856127
description: scientific article; zbMATH DE number 4039894