Static and user-extensible proof checking

DOI10.1145/2103656.2103690zbMath1321.68204OpenAlexW4253681328MaRDI QIDQ2942880

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

type theorydependent typesproof assistantsconversion ruletactic development

Mathematics Subject Classification ID

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

Related Items (1)

Mtac: A monad for typed tactic programming in Coq

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