A verified theorem prover backend supported by a monotonic library

DOI10.29007/F58NMaRDI QIDQ5222980zbMATH OpenOpenAlexFDO

Authors Vincent Rahli, Liron Cohen, Mark Bickford

Publication date 4 July 2019

Published in EPiC Series in Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.29007/f58n

zbMATH Keywords

monotonicityKripke semanticsCoqdigital libraryNuprlproof checkerverified theorem prover backend

Mathematics Subject Classification ID

Recommendations

• Towards a formally verified proof assistant
• scientific article; zbMATH DE number 4053566
• Metamath Zero: designing a theorem prover prover
• A verified runtime for a verified theorem prover
• Modular development of certified program verifiers with a proof assistant,

Cited in

(6)

• Formally computing with the non-computable
• A mechanised semantics for HOL with ad-hoc overloading
• Open bar -- a Brouwerian intuitionistic logic with a pinch of excluded middle
• Towards a formally verified proof assistant
• Experiences from exporting major proof assistant libraries
• scientific article; zbMATH DE number 7566056 (Why is no real title available?)

Describes a project that uses

Uses Software

• VeriPhy
• Idris
• Milawa
• Agda
• CakeML
• Nuprl
• HOL Light
• KeYmaera
• Eiffel
• Dafny
• Coq

This page was built for publication: A verified theorem prover backend supported by a monotonic library

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