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

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.