A verified theorem prover backend supported by a monotonic library

DOI10.29007/F58NzbMATH Open1409.68262OpenAlexW2906661256MaRDI QIDQ5222980FDOQ5222980

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

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,

zbMATH Keywords

monotonicityKripke semanticsCoqdigital libraryNuprlproof checkerverified theorem prover backend

Mathematics Subject Classification ID

Cited In (3)

• Formally computing with the non-computable
• Experiences from exporting major proof assistant libraries
• Title not available (Why is that?)

Uses Software

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

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)