Implementation choices Back-tracking in interactive proofs is implemented using the "timed" references of the Timed library. Bindings in terms are implemented using the Bindlib library. Parsing is using the Earley library.