Static and user-extensible proof checking

DOI10.1145/2103656.2103690MaRDI QIDQ2942880zbMATH OpenOpenAlexFDO

Authors Antonis Stampoulis, Zhong Shao

Publication date 11 September 2015

Published in Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2103656.2103690

zbMATH Keywords

dependent typestype theoryproof assistantsconversion ruletactic development

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Extensible and efficient automation through reflective tactics
• VeriML: typed computation of logical terms inside a language with effects
• Mtac: a monad for typed tactic programming in Coq
• Tactics and certificates in Meta Dedukti
• Mtac: a monad for typed tactic programming in Coq

Cited in

(3)

• On extensibility of proof checkers
• Mtac: a monad for typed tactic programming in Coq
• VeriML: typed computation of logical terms inside a language with effects

This page was built for publication: Static and user-extensible proof checking

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