English version

PPS UMR 7126 – Laboratoire
Preuves, Programmes et Systèmes

Accueil · Présentation · Membres · Publications · Séminaire · Groupes de travail · Projets · πr²

Arnaud Spiwack (Inria, Paris-Rocquencourt)

Coq's tactics in the future

I have been working on a branch of 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.