Difference between revisions of "VPL"
Jump to navigation
Jump to search
| Line 15: | Line 15: | ||
As a convenience, we distribute the OCaml library standalone, without any dependency on Coq developments. | As a convenience, we distribute the OCaml library standalone, without any dependency on Coq developments. | ||
| − | * [ | + | * [[:File:Vpl_caml_2013-05-16.zip|2013-05-16]] |
| + | * [[:File:VPL_2013-07-09.zip|2013-07-09]] includes F# version | ||
Revision as of 21:18, 9 July 2013
VPL is the {Verasco|VERIMAG} Polyhedra Library.
It consists in :
- An Objective Caml library, implementing polyhedral operations.
- A Coq checker and wrappers, which provably check the correctness (at least in one direction) of the polyhedral operations.
It implements the constraint-only algorithms for convex polyhedra found in [Fouilhe_et_al_SAS2013].
Prerequisites
- A recent version of OCaml with ocamlfind (findlib) and the ZArith library
- If using the Coq development: Coq 8.4pl1
Distribution
OCaml library
As a convenience, we distribute the OCaml library standalone, without any dependency on Coq developments.
- 2013-05-16
- 2013-07-09 includes F# version
