ThoR: An Alloy5-Like DSL for Interactive Theorem Proving in Coq

Abstract

The steep learning curve associated with interactive theorem proving poses a significant entry barrier for the learner. While the Alloy specification language [1] has simplified the introduction to and application of formal methods, transitioning to interactive theorem proving, such as with Coq [2], remains daunting due to the inherent complexity of formal reasoning and the sophisticated tooling required. We introduce ThoR, an extension for the Coq proof assistant that incorporates an Alloy5-like domain-specific language: Specifications, propositions and proofs are formulated in an Alloy5-like syntax. This reduces tool and language complexity, and makes interactive theorem proving more accessible. The implementation is based on Coq’s syntax extension capabilities and the mathematical components library (mathcomp) [4]. This paper reports on work in progress. It contributes an approach for the embedding of Alloy into Coq based on a set-theoretic interpretation, a proof calculus for Alloy with soundness by construction, a prototypical implementation and its validation via a simple token ring example.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{IglerM24,
  author       = {Bodo Igler and
                  Andreas Mayer},
  editor       = {Silvia Bonfanti and
                  Angelo Gargantini and
                  Michael Leuschel and
                  Elvinia Riccobene and
                  Patrizia Scandurra},
  title        = {ThoR: An Alloy5-Like {DSL} for Interactive Theorem Proving in Coq},
  booktitle    = {Rigorous State-Based Methods - 10th International Conference, {ABZ}
                  2024, Bergamo, Italy, June 25-28, 2024, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {14759},
  pages        = {248--254},
  publisher    = {Springer},
  year         = {2024},
  url          = {https://doi.org/10.1007/978-3-031-63790-2\_19},
  doi          = {10.1007/978-3-031-63790-2\_19},
  timestamp    = {Thu, 04 Jul 2024 22:05:23 +0200},
  biburl       = {https://dblp.org/rec/conf/zum/IglerM24.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}