L'action de recherche coopérative Concert a comme objectif principal de déterminer s'il est faisable, dans l'état actuel des connaissances, de réaliser un compilateur réaliste qui soit certifié, c'est-à-dire accompagné d'une preuve Coq d'équivalence sémantique entre le code source et le code machine engendré.
Cette action a démarré en Janvier 2003, après sélection par la direction de l'INRIA . Les documents fondateurs sont la proposition et son annexe. Il existe une liste de diffusion à laquelle il vous est possible de vous abonner en envoyant un courrier à cette adresse: sympa@lists-sop.inria.fr
La première réunion a eu lieu le 3 février 2003 à Sophia Antipolis. Vous pouvez accéder aux notes prise au cours de cette réunion
Coq à la conquête des moulins, Laurence Rideau and Bernard Serpette, JFLA'2005, Obernai, France, 9-10 Mars 2005. Associated source file.
A structured approach to proving compiler optimizations based on data-flow analysis, Yves Bertot, Benjamin Grégoire, and Xavier Leroy. Associated source file.
Last modified: Tue Jul 12 15:12:45 MEST 2005