Extensional constructs in intensional type theory
From MaRDI portal
Publication:4632162
DOI10.1007/978-1-4471-0963-1zbMATH Open1411.03001OpenAlexW1481180394MaRDI QIDQ4632162FDOQ4632162
Authors: Martin Hofmann 
Publication date: 26 April 2019
Full work available at URL: https://doi.org/10.1007/978-1-4471-0963-1
Recommendations
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)
Cited In (35)
- On strict and simple type extensions
- A minimalist two-level foundation for constructive mathematics
- Construction of tame types
- Title not available (Why is that?)
- Exact completion of path categories and algebraic set theory. I: Exact completion of path categories
- Typed Lambda Calculi and Applications
- Title not available (Why is that?)
- Title not available (Why is that?)
- Elementary fibrations of enriched groupoids
- Wellfounded trees in categories
- Title not available (Why is that?)
- 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
- From type theory to setoids and back
- Safe recursion with higher types and BCK-algebra
- 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
- An Extension of the Formulas-as-Types Paradigm
- Treatise on intuitionistic type theory
- Extensionality of \(\lambda^*\)
- Containers: Constructing strictly positive types
- Title not available (Why is that?)
- 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
- On generalized algebraic theories and categories with families
- Constructions of categories of setoids from proof-irrelevant 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)
