6 citations · 13 across the 9 of their papers we have counts for
12 papers
CIC + EM Con(ZF): the consistency of ZF in type theory with excluded middle and no choice
Mario Carneiro
The sets-as-trees interpretation of set theory in a dependent type theory with an impredicative universe of propositions validates Zermelo set theory, and it validates Replacement…
Definitional Inversion, Without Normalisation
Mario Carneiro, Thierry Coquand, Adrien Frabetti Mathieu +3
We contribute a new proof technique, based on domain theory, to prove key meta-theoretic properties of dependent type systems: definitional inversion properties, i.e. injectivity a…
Reimplementing Mizar in Rust
Mario Carneiro
This paper describes a new open-source proof processing tool, mizar-rs, a wholesale reimplementation of core parts of the Mizar proof system, written in Rust. In particular, the "c…
A Flexible Proof Format for SAT Solver-Elaborator Communication
Seulkee Baek, Mario Carneiro, Marijn J. H. Heule
We introduce FRAT, a new proof format for unsatisfiable SAT problems, and its associated toolchain. Compared to DRAT, the FRAT format allows solvers to include more information in…
Metamath Zero: The Cartesian Theorem Prover
Mario Carneiro
As the usage of theorem prover technology expands, so too does the reliance on correctness of the tools. Metamath Zero is a verification system that aims for simplicity of logic an…
Specifying verified x86 software from scratch
Mario Carneiro
We present a simple framework for specifying and proving facts about the input/output behavior of ELF binary files on the x86-64 architecture. A strong emphasis has been placed on…