| A monadic interpretation of tactics (2007) | |||||||||||||||
Abstract | |||||||||||||||
| Abstract. Many proof tools use ‘tactic languages ’ as programs to direct their proofs. We present a simplified idealised tactic language, and describe its denotational semantics. The language has many applications outside theorem-proving activities. The semantics is parametrised by a monad (plus additional structure). By instantiating this in various ways, the core semantics of a number of different tactic languages is obtained. 1 | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||