On the syntax of Martin-Löf's type theories

DOI10.1016/0304-3975(87)90047-8zbMath0638.03056OpenAlexW2068339813MaRDI QIDQ1099173

A. S. Troelstra

Publication date: 1987

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(87)90047-8

zbMATH Keywords

arithmetic fragment of Martin-Löf's type theoriesnormalization of terms

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50)

Related Items

Algebra of constructions II: an algebraic approach to Martin-Löf type theory and the calculus of constructions, European Summer Meeting of the Association for Symbolic Logic (Logic Colloquium '88), Padova, 1988, A note on Russell's paradox in locally Cartesian closed categories, Domain interpretations of Martin-Löf's partial type theory, An intuitionistic theory of types with assumptions of high-arity variables, Comprehension categories and the semantics of type dependency, Categorical and algebraic aspects of Martin-Löf type theory, Extended bar induction in applicative theories, Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\), Well-ordering proofs for Martin-Löf type theory

Uses Software

• Nuprl
• Automath

Cites Work

• Strong normalization for typed terms with surjective pairing
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Constructive mathematics and computer programming
• Semantics for classical AUTOMATH and related systems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item