Formalisation of VIPR: Verifying Integer Programming Results https://github.com/ambros-gleixner/VIPR
compilation: Compilation of VIPR proof checker
milpScript.sml: Formalisation of a syntax and semantics for MILP
real_plusScript.sml: Addition of linear terms with real-valued coefficients
sptree_unionWithScript.sml: Define unionWith for sptrees
viprProgScript.sml: Produces a verified CakeML program that checks VIPR proofs
vipr_checkerScript.sml: A pure version of the VIPR checker