The third tagged release of FreeSpec (git tag freespec.0.3) is built
upon the key idea of “monads morphisms,” and finally acknowledge the
relation between FreeSpec contracts and the Hoare logic. Besides, it
is also the release which motivates the development of the coqffi
tool. Finally, it is the
first tagged release to be distributed under the terms of the MPL
2.0.
The second tagged release of FreeSpec (git tag freespec-r2) is
described in depth in “FreeSpec: Specifying, Certifying and Executing
Impure Computations in Coq”. The
focus of this release is programming and verifying “in the small,”
i.e., it introduces many concepts with allow to reuse programs and
proofs. Besides, it first features the Exec vernacular command, to
execute from within Coq effectful programs.
The first tagged release of FreeSpec (git tag freespec-r1) is
described in depth in “Modular Verification of Programs with Effects
and Effect Handlers in Coq”. The
focus of this release is programming and verifying “in the large,”
i.e., it establishes the foundation of the formalism.