The implementation presented here is intended as a factual
description as opposed to code meant for direct and immediate use.
The implementation is given in
Coq,
but translates directly to any statically typed functional language
(and can probably be automatically extracted to OCaml and Haskell
code without much effort). Full source for the Coq development is
available in
Procedure.v.