Sets in types, types in sets

DOI10.1007/BFB0014566MaRDI QIDQ4364399zbMATH OpenFDO

Authors Benjamin Werner

Publication date 15 April 1998

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BFB0014566

zbMATH Keywords

Calculus of Inductive Constructionsencodingsexpressive powergeneralization of Coquand's simple proof-irrelevance interpretationinaccessible cardinalstype theoryuniversesvariant of Aczel's encodingZermelo-Fraenkel set theory

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Applications of set theory (03E75)

Recommendations

• On relating type theories and set theories
• Sets in Coq, Coq in Sets
• Categoricity results for second-order ZF in dependent type theory
• Characterizing the interpretation of set theory in Martin-Löf type theory

Cited in

(34)

• A compact kernel for the calculus of inductive constructions
• Categoricity results for second-order ZF in dependent type theory
• Typing total recursive functions in Coq
• Categoricity results and large model constructions for second-order ZF in dependent type theory
• Extensible and efficient automation through reflective tactics
• Encoding functional relations in Scunak
• Sets in Coq, Coq in Sets
• Types, Sets, and Categories
• Combining Type Theory and Untyped Set Theory
• Sets, types and type-checking
• On relating type theories and set theories
• Trakhtenbrot’s Theorem in Coq
• Formalization of Forcing in Isabelle/ZF
• scientific article; zbMATH DE number 7566073 (Why is no real title available?)
• Impredicative encodings of (higher) inductive types
• W-types in setoids
• Formal proof of Banach-Tarski paradox
• A foundational view on integration problems
• scientific article; zbMATH DE number 7649968 (Why is no real title available?)
• From type theory to setoids and back
• Types for Proofs and Programs
• What is the point of computers? A question for pure mathematicians
• The formal verification of the ctm approach to forcing
• Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version
• Wetzel: formalisation of an undecidable problem linked to the continuum hypothesis
• An intuitionistic set-theoretical model of fully dependent CC
• Encoding type universes without using matching modulo associativity and commutativity
• Touring the MetaCoq project
• ``Upon this quote I will build my Church thesis
• The category of iterative sets in homotopy type theory and univalent foundations
• Completeness of first-order bi-intuitionistic logic
• Strong Normalization of Moggis's Computational Metalanguage
• Explaining Gabriel-Zisman localization to the computer
• Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Sets in types, types in sets

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