A verified runtime for a verified theorem prover

DOI10.1007/978-3-642-22863-6_20MaRDI QIDQ3088011zbMATH OpenOpenAlexFDO

Authors Magnus O. Myreen, Jared Davis

Publication date 17 August 2011

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

Full work available at URL https://doi.org/10.1007/978-3-642-22863-6_20

Mathematics Subject Classification ID

Recommendations

• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• A verified compiler from Isabelle/HOL to CakeML
• Metamath Zero: designing a theorem prover prover
• CakeML

Cites work

• scientific article; zbMATH DE number 193479 (Why is no real title available?)
• scientific article; zbMATH DE number 1301853 (Why is no real title available?)
• scientific article; zbMATH DE number 771699 (Why is no real title available?)
• A Brief Overview of HOL4
• A certified framework for compiling and executing garbage-collected languages
• A verified compiler for an impure functional language
• Edinburgh LCF. A mechanized logic of computation
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• HOL Light: An Overview
• Mechanized Verification of CPS Transformations
• Recursive functions of symbolic expressions and their computation by machine, Part I
• Theorem Proving in Higher Order Logics
• Towards Self-verification of HOL Light
• Verified just-in-time compiler on x86

Cited in

(10)

• Computer Aided Verification
• A verified generational garbage collector for CakeML
• LCF-style bit-blasting in HOL4
• Runtime Verification with Imperfect Information Through Indistinguishability Relations
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• The verified CakeML compiler backend
• Candle: a verified implementation of HOL Light (extended version)
• A verified generational garbage collector for CakeML
• A verified theorem prover backend supported by a monotonic library

Describes a project that uses

Uses Software

• GCminor
• Milawa
• NQTHM
• HOL Light
• OCaml
• HOL
• VLISP
• Isabelle
• Coq
• ACL2

This page was built for publication: A verified runtime for a verified theorem prover

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3088011)