Arnaud Spiwack (Inria, Paris-Rocquencourt)

Coq's tactics in the future

I have been working on a branch of Coq ( https://github.com/aspiwack/coq ) which brings new features to the tactic language of Coq. These features dependent subgoals, multiple-goal to multiple-goal tactics and backtracking primitives.

After presenting these features, we will dive into the insides of the supporting OCaml code. I will describe the abstract interface which I designed to replace the old LCF-inspired concrete interface. The interface, as it happens, exposes monadic constructs. I will then explain how this interface is implemented. This will make me consider impredicative encodings and transactional memory.