An operational foundation for the tactic language of Coq
Wojciech Jedynak, Małgorzata Biernacka, Dariusz Biernacki · 2013
We introduce a semantic toolbox for Ltac, the tactic language of the popular Coq proof assistant. We present three formats of operational semantics, each of which has its use in the practice of tactic programming: a big-step specification in the form of natural semantics, a model of implementation in the form of an abstract machine, and a small-step characterization of computation in the form of reduction semantics. The three semantics are provably equivalent and have been obtained via off-the-shelf derivation techniques of the functional correspondence and the syntactic correspondence. We also give examples of Ltac programs and discuss some of the issues that the formal semantics help to clarify.