Static and user-extensible proof checking

DOI10.1145/2103656.2103690zbMATH Open1321.68204OpenAlexW4253681328MaRDI QIDQ2942880FDOQ2942880

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

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

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)

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)