scientific article; zbMATH DE number 1088050
From MaRDI portal
Publication:4364399
zbMath0885.03017MaRDI QIDQ4364399
Publication date: 15 April 1998
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
expressive powertype theoryuniversesencodingsZermelo-Fraenkel set theoryinaccessible cardinalsCalculus of Inductive Constructionsgeneralization of Coquand's simple proof-irrelevance interpretationvariant of Aczel's encoding
Related Items (18)
From type theory to setoids and back ⋮ Trakhtenbrot’s Theorem in Coq ⋮ Formalization of Forcing in Isabelle/ZF ⋮ Explaining Gabriel-Zisman localization to the computer ⋮ Categoricity results for second-order ZF in dependent type theory ⋮ Typing total recursive functions in Coq ⋮ 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 ⋮ Unnamed Item ⋮ An intuitionistic set-theoretical model of fully dependent CC ⋮ Unnamed Item ⋮ A Foundational View on Integration Problems ⋮ Extensible and Efficient Automation Through Reflective Tactics ⋮ Categoricity results and large model constructions for second-order ZF in dependent type theory ⋮ A compact kernel for the calculus of inductive constructions ⋮ Formal Proof of Banach-Tarski Paradox
Uses Software
This page was built for publication:
