Jeudi 09/09/2010, à partir de 16h, en salle Galois Coriolis.
Orateur : Sylvain Heraud.
Titre : Formaliser des fonctions polynomiales en Coq.
Résumé :
Nous présenterons deux classes de complexité, Cobham [Cob64] et Bellantoni/Cook [BS92], qui permettent de décrire tout les programmes polynomiales (et uniquement les programmes polynomiales). L’article de Bellantoni et Cook [BC92] montre que ces deux classes sont équivalentes, nous vous montrerons comment on peut traduire cette preuve en un compilateur certifie en Coq. Ces résultats pourront être utiliser en Cryptographie [BGZ09, Now07], ou en Complexite [SJ03] (si vous en connaissez d’autres preuves qui on besoin de la notion « Polytime » je suis preneur). Ça peut être un premier pas vers la formalisation de classes plus complexes comme [Hof00] ou plus récemment [Zha09].[BGZ09] G. Barthe, B. Gregoire, and S. Zanella Béguelin. Formal certification of code-based cryptographic proofs. POPL.
[BC92] S. Bellantoni and S.A. Cook. A new recursion-theoretic characterization of the polytime functions. Computational Complexity.
[Cob64] A. Cobham. The intrinsic computational difficulty of functions. International Congress for Logic, Methodology, and the Philosophy of Science.
[Hof00] M. Hofmann. Safe recursion with higher types and BCK-algebra. Annals of Pure and Applied Logic.
[Now07] D. Nowak. A framework for game-based security proofs. ICICS 2007.
[SJ03] C. Schurmann and J. Shah. Representing reductions of NP-complete problems in logical frameworks: a case study. MERLIN.
[Zha09] Y. Zhang. The Computational SLR: A Logic for Reasoning about Computational Indistinguishability. TLCA.
