Vous pouvez vous abonner à nos annonces de séminaires
		    http://gallium.inria.fr/seminaires/

			     S E M I N A I R E
			   __
			  / _`  _   /  /  o
			 /   ) __) /  /  / /  / /\/|
			(___/ (_/ (_ (_ / (__/ /   |

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 1, bâtiment C

                           Lundi 3 septembre, 10h30

                               ---------------
                               Damien Rouhling
                               ---------------

                     Inria Sophia Antipolis Méditerranée

                         ===========================
                         Asymptotic Reasoning in Coq
                         ===========================

Formalizing analysis on a computer involves a lot of epsilon/delta reasoning,
while informal reasoning may use some asymptotic hand-waving. Having to provide
explicit deltas early in the proof makes the proof less stable and less readable
than it would be with a correct informal reasoning. We present formalization
techniques that take advantage of existential variables to delay the input of
existential witnesses until a stage where the proof assistant can actually infer
them. We used these techniques to prove theorems about classical analysis in Coq
and to provide equational Bachmann-Landau notations. This partially restores the
simplicity of informal hand-waving without compromising the proof. As expected
this also reduces the size of proof scripts and the time to write them, and it
also makes proofs more stable.
This is joint work with Reynald Affeldt and Cyril Cohen.