The Reflective Milawa Theorem Prover Is Sound

DOI10.1007/978-3-319-08970-6_27zbMath1416.68174OpenAlexW2230207899MaRDI QIDQ2879267

Jared Davis, Magnus O. Myreen

Publication date: 8 September 2014

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-08970-6_27

Mathematics Subject Classification ID

Related Items (7)

Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation ⋮ Aligning concepts across proof assistant libraries ⋮ Proof-Producing Reflection for HOL ⋮ A Consistent Foundation for Isabelle/HOL ⋮ A consistent foundation for Isabelle/HOL ⋮ Milawa ⋮ Jitawa

Uses Software

• ACL2
• Coq
• HOL
• CakeML

This page was built for publication: The Reflective Milawa Theorem Prover Is Sound