Mario Carneiro
- Metamath Zero: The Cartesian Theorem Prover
2019/10/22 by Mario Carneiro, Carneiro, Mario · 3 voices
Computer Science · #Logic, programming, and type systems #Security and Verification in Computing #Formal Methods in Verification
- Lean4Lean: Verifying a Typechecker for Lean, in Lean
2024/03/21 by Mario Carneiro, Carneiro, Mario · 3 voices · 5 citations
Computer Science · Engineering · #D.2.4 #F.4.1 #FOS: Computer and information sciences #Flexible and Reconfigurable Manufacturing Systems #G.4 #Manufacturing Process and Optimization #Programming Languages (cs.PL) #cs.PL
- Formal Verification of the Empty Hexagon Number
2024/03/26 by Bernardo Subercaseaux, Subercaseaux, Bernardo, Wojciech J. Nawrocki +9 · 4 citations
Computer Science · #Computational Geometry (cs.CG) #Constraint Satisfaction and Optimization #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Polynomial and algebraic computation
- Conversion of HOL Light proofs into Metamath
2014/12/18 by Mario Carneiro, Carneiro, Mario · 1 citation
Computer Science · #Logic, programming, and type systems #Logic, Reasoning, and Knowledge #Semantic Web and Ontologies
- Models for Metamath
2016/01/28 by Mario Carneiro, Carneiro, Mario · 1 citation
Computer Science · #03B22 #03B70 (Secondary) #03C95 (Primary) #Advanced Database Systems and Queries #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #I.2.3 #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems