I read the report: “A full formalisation of BLP model” and find Coq code.
But I can’t run this code. Maybe I do this wrong.
Please tell me if you can run it.
This file is for Coq 7.3 (a very old version released in 2002). Since then, many things have changed, including the syntax. Unfortunately getting such an old release is quite an endeavor since it expected OCaml 3.01 which is too old to find on opam.
1 Like