Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC

Yuhui Lin, Gudmund Grov, Rob Arthan

The use of a functional language to implement proof strategies as proof tactics in interactive theorem provers, often provides short, concise and elegant implementations. Whilst be…