Extensional constructs in intensional type theory

DOI10.1007/978-1-4471-0963-1MaRDI QIDQ4632162zbMATH OpenOpenAlexFDO

Authors Martin Hofmann

Publication date 26 April 2019

Full work available at URL https://doi.org/10.1007/978-1-4471-0963-1

Mathematics Subject Classification ID

Theory of programming languages (68N15) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Logic in computer science (03B70) Semantics in the theory of computing (68Q55)

Recommendations

• Treatise on intuitionistic type theory
• scientific article; zbMATH DE number 50149
• scientific article; zbMATH DE number 591911
• Type theory and formal proof. An introduction
• Conservativity of equality reflection over intensional type theory

Cited in

(35)

• On strict and simple type extensions
• A minimalist two-level foundation for constructive mathematics
• Construction of tame types
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• Exact completion of path categories and algebraic set theory. I: Exact completion of path categories
• Typed Lambda Calculi and Applications
• scientific article; zbMATH DE number 7269245 (Why is no real title available?)
• scientific article; zbMATH DE number 1302055 (Why is no real title available?)
• Elementary fibrations of enriched groupoids
• Wellfounded trees in categories
• scientific article; zbMATH DE number 6680163 (Why is no real title available?)
• Guarded cubical type theory
• Conservativity of equality reflection over intensional type theory
• Principal type schemes for an extended type theory
• Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice
• Game semantics for dependent types
• Safe recursion with higher types and BCK-algebra
• From type theory to setoids and back
• A Comparison of Type Theory with Set Theory
• Extensional and Intensional Semantic Universes
• Variations on Noetherianness
• Eta-rules in Martin-Löf type theory
• The effective model structure and \(\infty\)-groupoid objects
• From rewrite rules to axioms in the \(\lambda \varPi \)-calculus modulo theory
• Treatise on intuitionistic type theory
• An Extension of the Formulas-as-Types Paradigm
• Containers: Constructing strictly positive types
• Extensionality of \(\lambda^*\)
• scientific article; zbMATH DE number 5316130 (Why is no real title available?)
• Quotienting the delay monad by weak bisimilarity
• (In)consistency of Extensions of Higher Order Logic and Type Theory
• A computer-verified monadic functional implementation of the integral
• Constructions of categories of setoids from proof-irrelevant families
• On generalized algebraic theories and categories with families
• The compatibility of the minimalist foundation with homotopy type theory

This page was built for publication: Extensional constructs in intensional type theory

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