- Sophie Bernard
- Yves Bertot,
- Jean-Yves Franceschi
- Laurence Rideau
- Pierre-Yves Strub
Public documents developed in the Marelle team
Formal proofs :
Most of the formal proofs developed in the team are available somewhere else. This page provides
a temporary access venue for documents that do not yet have better place to reside on the web.
Jean-Yves Franceschi internship (2015) :
A formal study of a description differential dynamic logic in Coq: source code. This code was compiled
and tested with coq-8.4pl4, ssreflect-1.5, math-comp-1.5, and coquelicot-2.1.0.
Proof of transcendence for e and pi (2015) :
A paper has been submitted for publication on this topic. This is the associated source code (version of Oct. 15, 2015).
The final results are the last lemmas in files trans_e.v and trans_pi.v. To run this source code, there are a few possibilities:
- If you have an installed version of coq-8.4pl6, ssreflect-1.5, mathcomp-1.5, coquelicot-2.1.0, accessible
through the PATH variable. you can just extract the contents of the archive, go to the transcendence directory, and type
- If you already use opam, you can set up the required environment and compile our code in the following fashion:
opam repository add coq-released https://coq.inria.fr/opam/released
opam repository add coq-extra-dev https://coq.inria.fr/opam/extra-dev
opam install coq.8.4.6 coq:math-comp.1.5.0 coq:coquelicot.2.1.0
You can then extract the contents of the archive, go to the transcendence directory, and type
- If you want to build a temporary installation of all the require software, you can extract the contents of the archive,
go to the transcendance directory antype the following command:
This will build a suitable version of Coq and the required libraries in the
directory ../transcendence/_tools/ and then compile our development using that version of coq.