Sur cette page se trouve tout le matériel correspondant à ma thèse (manuscrit, scripts, liste de correspondances entre les noms dans la these et dans les fichiers). Elle a été soutenue le 15 juin 2012 devant un jury composé de :
News: the whole stuff with implementation, makefile, installation instructions and liste of correspondences with thesis items, tested for Coq 8.4 beta (Remark of July 2015 by Ralph Matthes: the files still compile fine with Coq 8.4pl6 - regardless of whether with provided makefile or the one generated with coq_makefile from Coq 8.4pl6.)
News 2016: the whole stuff with implementation and Coq-generated makefile, tested for Coq 8.5pl1 (but excluding the correspondences, that are still mostly correct, and installation instructions - just run make)