implementation.md

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.