scientific article; zbMATH DE number 1420782
From MaRDI portal
Publication:4944846
calculus of constructionsclassical set theoryconstructive set theoryconstructive type theoryinaccessible cardinalinaccessible setsproof development systems Lego and Coqproof-theoretic strengthsets-as-trees interpretationtype universetypes-as-sets interpretation
Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) Nonclassical and second-order set theories (03E70) Proof theory in general (including proof-theoretic semantics) (03F03) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50)
Recommendations
- Characterizing the interpretation of set theory in Martin-Löf type theory
- Universes in type theory. I. Inaccessibles and Mahlo
- The strength of some Martin-Löf type theories
- Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions
- scientific article; zbMATH DE number 1088050
Cited in
(44)- The strength of some Martin-Löf type theories
- Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017
- Canonicity and normalization for dependent type theory
- Containers: Constructing strictly positive types
- Heyting-valued interpretations for constructive set theory
- Reconsidering pairs and functions as sets
- Transfinite constructions in classical type theory
- Extending type theory with forcing
- Relations Versus Functions at the Foundations of Logic: Type-Theoretic Considerations
- Sets in Coq, Coq in Sets
- scientific article; zbMATH DE number 4172399 (Why is no real title available?)
- In the Search of a Naive Type Theory
- On the strength of proof-irrelevant type theories
- Combining Type Theory and Untyped Set Theory
- On the Strength of Proof-Irrelevant Type Theories
- Relating first-order set theories, toposes and categories of classes
- Collections, sets and types
- scientific article; zbMATH DE number 1088050 (Why is no real title available?)
- scientific article; zbMATH DE number 1088206 (Why is no real title available?)
- Cubical type theory: a constructive interpretation of the univalence axiom
- scientific article; zbMATH DE number 2085163 (Why is no real title available?)
- Internal universes in models of homotopy type theory
- Cumulative inductive types in Coq
- Canonicity and homotopy canonicity for cubical type theory
- Constructive sheaf models of type theory
- Homotopy canonicity for cubical type theory
- W-types in setoids
- Homotopy type-theoretic interpretations of constructive set theories
- A foundational view on integration problems
- Proof theory of constructive systems: inductive types and univalence
- Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions
- A Normalizing Intuitionistic Set Theory with Inaccessible Sets
- Universes in type theory. I. Inaccessibles and Mahlo
- The generalised type-theoretic interpretation of constructive set theory
- From type theory to setoids and back
- Type inference for set theory
- A presheaf model of parametric type theory
- Is sized typing for Coq practical?
- An intuitionistic set-theoretical model of fully dependent CC
- On specifications, subset types and interpretation of proposition in type theory
- The category of iterative sets in homotopy type theory and univalent foundations
- The equivariant model structure on cartesian cubical sets
- Explaining Gabriel-Zisman localization to the computer
- Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4944846)
