scientific article
From MaRDI portal
Publication:3075242
zbMath1211.03023MaRDI QIDQ3075242
Publication date: 10 February 2011
Full work available at URL: http://jfr.cib.unibo.it/article/view/1695
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Coqinaccessible cardinalsHFZFhereditarily finite setsreplacement axiomCalculus of Inductive Constructionsset-theoretical models
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (19)
From type theory to setoids and back ⋮ Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation ⋮ From realizability to induction via dependent intersection ⋮ Parametric Church's thesis: synthetic computability without choice ⋮ A Consistent Foundation for Isabelle/HOL ⋮ Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language ⋮ Categoricity results for second-order ZF in dependent type theory ⋮ Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version ⋮ An intuitionistic set-theoretical model of fully dependent CC ⋮ A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL ⋮ A solution to the PoplMark challenge based on de Bruijn indices ⋮ Comprehending Isabelle/HOL’s Consistency ⋮ A consistent foundation for Isabelle/HOL ⋮ Extensible and Efficient Automation Through Reflective Tactics ⋮ Type Theory Should Eat Itself ⋮ \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic ⋮ Categoricity results and large model constructions for second-order ZF in dependent type theory ⋮ Formalizing Arrow's theorem ⋮ A formalization and proof checker for Isabelle's metalogic
Uses Software
This page was built for publication:
