A Verified Theorem Prover Backend Supported by a Monotonic Library

DOI10.29007/f58nzbMath1409.68262OpenAlexW2906661256MaRDI QIDQ5222980

Liron Cohen, Mark Bickford, Vincent Rahli

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

Related Items (3)

Unnamed Item ⋮ Experiences from exporting major proof assistant libraries ⋮ Formally computing with the non-computable

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