scientific article; zbMATH DE number 1420782
zbMATH Open0944.03056MaRDI QIDQ4944846FDOQ4944846
Authors: Peter Aczel 
Publication date: 20 September 2000
Title of this publication is not available (Why is that?)
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
constructive set theoryinaccessible cardinalproof-theoretic strengthconstructive type theorycalculus of constructionsinaccessible setssets-as-trees interpretationclassical set theoryproof development systems Lego and Coqtype universetypes-as-sets interpretation
Proof theory in general (including proof-theoretic semantics) (03F03) Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) Nonclassical and second-order set theories (03E70) Metamathematics of constructive systems (03F50) Second- and higher-order arithmetic and fragments (03F35)
Cited In (38)
- Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017
- Extending type theory with forcing
- A Normalizing Intuitionistic Set Theory with Inaccessible Sets
- Explaining Gabriel-Zisman localization to the computer
- Canonicity and homotopy canonicity for cubical type theory
- Transfinite constructions in classical type theory
- Title not available (Why is that?)
- Title not available (Why is that?)
- The strength of some Martin-Löf type theories
- Proof theory of constructive systems: inductive types and univalence
- Reconsidering pairs and functions as sets
- On the strength of proof-irrelevant type theories
- A foundational view on integration problems
- An intuitionistic set-theoretical model of fully dependent CC
- From type theory to setoids and back
- Type inference for set theory
- Combining Type Theory and Untyped Set Theory
- Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics
- W-types in setoids
- Title not available (Why is that?)
- Sets in Coq, Coq in Sets
- The generalised type-theoretic interpretation of constructive set theory
- On specifications, subset types and interpretation of proposition in type theory
- Cumulative inductive types in Coq
- In the Search of a Naive Type Theory
- Containers: Constructing strictly positive types
- On the Strength of Proof-Irrelevant Type Theories
- Constructive sheaf models of type theory
- Cubical type theory: a constructive interpretation of the univalence axiom
- Internal universes in models of homotopy type theory
- Universes in type theory. I. Inaccessibles and Mahlo
- Heyting-valued interpretations for constructive set theory
- Is sized typing for Coq practical?
- Canonicity and normalization for dependent type theory
- Relations Versus Functions at the Foundations of Logic: Type-Theoretic Considerations
- Relating first-order set theories, toposes and categories of classes
- A presheaf model of parametric type theory
- Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions
Uses Software
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)
