Mario Carneiro

Publication Activity (10 Years)

Years Active: 2014-2024
Publications (10 Years): 19

Top Topics

Formal Verification

Clause Learning Sat Solvers

Propositional Satisfiability

Top Venues

FM4M/MathUI/ThEdu/DP/WIP@CIKM

Formaliz. Math.

Publications

Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden R. Codel, Mario Carneiro, Marijn J. H. Heule
Formal Verification of the Empty Hexagon Number. CoRR (2024)
Mario Carneiro
Lean4Lean: Towards a formalized metatheory for the Lean theorem prover. CoRR (2024)
Mario Carneiro
Reimplementing Mizar in Rust. CoRR (2023)
Mario Carneiro, Chad E. Brown, Josef Urban
Automated Theorem Proving for Metamath. ITP (2023)
Mario Carneiro
Reimplementing Mizar in Rust. ITP (2023)
Mario Carneiro
The Divergence of the Sum of Prime Reciprocals. Formaliz. Math. 30 (3) (2022)
Seulkee Baek, Mario Carneiro, Marijn J. H. Heule
A Flexible Proof Format for SAT Solver-Elaborator Communication. Log. Methods Comput. Sci. 18 (2) (2022)
Seulkee Baek, Mario Carneiro, Marijn J. H. Heule
A Flexible Proof Format for SAT Solver-Elaborator Communication. TACAS (1) (2021)
Seulkee Baek, Mario Carneiro, Marijn J. H. Heule
A Flexible Proof Format for SAT Solver-Elaborator Communication. CoRR (2021)
Mario Carneiro
Metamath Zero: Designing a Theorem Prover Prover. CICM (2020)
Mario Carneiro
Metamath Zero: The Cartesian Theorem Prover. CoRR (2019)
Mario Carneiro
Specifying verified x86 software from scratch. CoRR (2019)
Jeremy Avigad, Mario Carneiro, Simon Hudon
Data Types as Quotients of Polynomial Functors. ITP (2019)
Mario Carneiro
Formalizing Computability Theory via Partial Recursive Functions. ITP (2019)
Mario Carneiro
Formalizing computability theory via partial recursive functions. CoRR (2018)
Mario Carneiro
Formalization of the prime number theorem and Dirichlet's theorem. FM4M/MathUI/ThEdu/DP/WIP@CIKM (2016)
Mario Carneiro
Models for Metamath. FM4M/MathUI/ThEdu/DP/WIP@CIKM (2016)
Mario Carneiro
Conversion of HOL Light proofs into Metamath. J. Formaliz. Reason. 9 (1) (2016)
Mario Carneiro
Models for Metamath. CoRR (2016)
Mario Carneiro
Arithmetic in Metamath, Case Study: Bertrand's Postulate. CICM (Work in Progress) (2015)
Mario Carneiro
Arithmetic in Metamath, Case Study: Bertrand's Postulate. CoRR (2015)
Mario Carneiro
Conversion of HOL Light proofs into Metamath. CoRR (2014)