My defence took place on Tuesday November 20 at 2 p.m. in amphitheatre Monge in “École polytechnique”, with the following jury:

Thesis

Here is the final version, and the BibTex.
Summary here / Résumé ici.

Coq Source code

Here is the Coq source code for the formalizations described in my thesis, you need ssreflect to compile it. Note that some files are in the 1.4 release of ssreflect (ssrnum.v, ssrint.v, rat.v, generic_quotient.v). If something is missing, please tell me.
These sources contain:


This page was last updated at 2014-12-01 03:52:16 +0100
This site is compiled with nanoc and hosted by Cr@ns

Warning: fopen(index.log): failed to open stream: Permission denied in /home/cohen/www/phd/index.php on line 91

Warning: fwrite() expects parameter 1 to be resource, bool given in /home/cohen/www/phd/index.php on line 92

Warning: Use of undefined constant REMOTE_HOST - assumed 'REMOTE_HOST' (this will throw an Error in a future version of PHP) in /home/cohen/www/phd/index.php on line 93

Notice: Undefined index: REMOTE_HOST in /home/cohen/www/phd/index.php on line 93

Warning: Use of undefined constant REMOTE_ADDR - assumed 'REMOTE_ADDR' (this will throw an Error in a future version of PHP) in /home/cohen/www/phd/index.php on line 93

Warning: fwrite() expects parameter 1 to be resource, bool given in /home/cohen/www/phd/index.php on line 93

Warning: fclose() expects parameter 1 to be resource, bool given in /home/cohen/www/phd/index.php on line 94