Categorical and algebraic aspects of Martin-Löf type theory

DOI10.1007/BF00370827MaRDI QIDQ750438zbMATH OpenOpenAlexFDO

Authors Adam Obtułowicz

Publication date 1989

Published in Studia Logica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf00370827

zbMATH Keywords

Cartesian closed categoryindexed categorylambda calculusMartin- Löf Type Theory

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50) Categorical logic, topoi (03G30) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15)

Recommendations

• Algebra of constructions II: an algebraic approach to Martin-Löf type theory and the calculus of constructions
• AN INTERPRETATION OF MARTIN‐LÖF'S CONSTRUCTIVE THEORY OF TYPES IN ELEMENTARY TOPOS THEORY
• Locally cartesian closed categories and type theory
• On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory
• Indexed type theories

Cites work

• Aspects of topoi
• Generalized algebraic theories and contextual categories
• scientific article; zbMATH DE number 3959364 (Why is no real title available?)
• scientific article; zbMATH DE number 3605078 (Why is no real title available?)
• scientific article; zbMATH DE number 3367095 (Why is no real title available?)
• Locally cartesian closed categories and type theory
• On the syntax of Martin-Löf's type theories
• Recursive models for constructive set theories

Cited in

(12)

• Wellfounded trees in categories
• scientific article; zbMATH DE number 4177054 (Why is no real title available?)
• Locally cartesian closed categories and type theory
• Algebra of constructions II: an algebraic approach to Martin-Löf type theory and the calculus of constructions
• Categorical structures for type theory in univalent foundations
• Martin Hofmann’s contributions to type theory: Groupoids and univalence
• scientific article; zbMATH DE number 7204300 (Why is no real title available?)
• Indexed type theories
• On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory
• Algebra and Coalgebra in Computer Science
• Martin-Löf identity types in C-systems
• Polynomial-time Martin-Löf type theory

This page was built for publication: Categorical and algebraic aspects of Martin-Löf type theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q750438)