Contributors :

- 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
    make
  • 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
    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 build-via-toolchain
    
    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.