Algebra of constructions II: an algebraic approach to Martin-Löf type theory and the calculus of constructions

DOI10.1017/S0960129500000128zbMath0803.03045OpenAlexW2067344494MaRDI QIDQ4279249

Adam Obtułowicz

Publication date: 16 February 1994

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0960129500000128

zbMATH Keywords

decidabilitycalculus of constructionssemanticssyntaxalgebraic approachrecursive structuresemantical domainsessentially algebraic theoriesthree-sorted partial algebrasmodels of Martin-Löf type theory

Mathematics Subject Classification ID

Applications of universal algebra in computer science (08A70) Semantics in the theory of computing (68Q55) Other algebras related to logic (03G25) Second- and higher-order arithmetic and fragments (03F35) Partial algebras (08A55)

Cites Work

• Unnamed Item
• Unnamed Item
• On the syntax of Martin-Löf's type theories
• Algebra of constructions. I. The word problem for partial algebras
• The calculus of constructions
• Near-equational and equational systems of logic for partial functions. I
• Locally cartesian closed categories and type theory
• Initial Algebra Semantics and Continuous Algebras

This page was built for publication: Algebra of constructions II: an algebraic approach to Martin-Löf type theory and the calculus of constructions