scientific article; zbMATH DE number 1420782

zbMath0944.03056MaRDI QIDQ4944846

Peter Aczel

Publication date: 20 September 2000

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

calculus of constructionsconstructive type theoryproof-theoretic strengthinaccessible cardinalconstructive set theoryinaccessible setssets-as-trees interpretationclassical set theoryproof development systems Lego and Coqtype universetypes-as-sets interpretation

Mathematics Subject Classification ID

Logic in computer science (03B70) Mechanization of proofs and logical operations (03B35) Nonclassical and second-order set theories (03E70) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50) Proof theory in general (including proof-theoretic semantics) (03F03)

Related Items (20)

From type theory to setoids and back ⋮ Reconsidering pairs and functions as sets ⋮ Explaining Gabriel-Zisman localization to the computer ⋮ Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics ⋮ Constructive sheaf models of type theory ⋮ Unnamed Item ⋮ Canonicity and normalization for dependent type theory ⋮ Is sized typing for Coq practical? ⋮ Canonicity and homotopy canonicity for cubical type theory ⋮ An intuitionistic set-theoretical model of fully dependent CC ⋮ A presheaf model of parametric type theory ⋮ Cumulative Inductive Types in Coq ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017 ⋮ Cubical Type Theory: a constructive interpretation of the univalence axiom ⋮ Unnamed Item ⋮ A Foundational View on Integration Problems ⋮ Proof Theory of Constructive Systems: Inductive Types and Univalence ⋮ Containers: Constructing strictly positive types ⋮ Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions ⋮ Heyting-valued interpretations for constructive set theory

Uses Software

• Coq
• LEGO

This page was built for publication: