2 citations · 3 across the 2 of their papers we have counts for
4 papers
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…
Formalizing computability theory via partial recursive functions
Mario Carneiro
We present an extension to the library of the Lean theorem prover formalizing the foundations of computability theory. We use primitive recursive functions and p…
GCH implies AC, a Metamath Formalization
Mario Carneiro
We present the formalization of Specker's "local" version of the claim that the Generalized Continuum Hypothesis implies the Axiom of Choice, with particular attention to some extr…