A tactic calculus — abridged version
Andrew Martin, P. H. B. Gardiner, Jim Woodcock · Formal Aspects of Computing · 1996
Abstract We present a very general language for expressing tactic programs. The paper describes some essential tactic combinators (tacticals), and gives them a formal semantics. Those definitions are used to produce a complete calculus for reasoning about tactics written in this language. The language is extended to cover structural combinators which enable the tactics to be precisely targeted upon particular sub-expressions.