Contributors :
 Sophie Bernard
 Yves Bertot,
 JeanYves Franceschi
 Laurence Rideau
 PierreYves 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.
JeanYves Franceschi internship (2015) :
A formal study of a description differential dynamic logic in Coq: source code. This code was compiled and tested with coq8.4pl4, ssreflect1.5, mathcomp1.5, and coquelicot2.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 coq8.4pl6, ssreflect1.5, mathcomp1.5, coquelicot2.1.0, accessible
through the PATH variable. you can just extract the contents of the archive, go to the transcendence directory, and type
make
 If you already use opam, you can set up the required environment and compile our code in the following fashion:
opam repository add coqreleased https://coq.inria.fr/opam/released
opam repository add coqextradev https://coq.inria.fr/opam/extradev
opam install coq.8.4.6 coq:mathcomp.1.5.0 coq:coquelicot.2.1.0
You can then extract the contents of the archive, go to the transcendence directory, and type make
 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:
make toolchain
make buildviatoolchain
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.
