Jean-Francois Monin              
                     Verimag Grenoble - 2004            
                 http://www-verimag.imag.fr/~monin/
---------------------------------------------------------------------
                       Version for Coq 8.0
---------------------------------------------------------------------

We provide a formal proof that the elegant trick of Olivier Danvy for
expressing printf-like functions without dependent types is correct,
where formats are encoded by functional expressions in
continuation-passing style.

We stress a methodological point: when one proves equalities between
functions, a common temptation is to introduce a comprehension axiom
and then to prove that the considered functions are extensionally
equal.  Rather than weakening the result (and adding an axiom), we
prefer to strenghten the inductive argumentation in order to stick to
the intensional equality.

---------------------------------------------------------------------

FILES:

                             combi.v
         (basic definitions such as sequential composition)
                               |
                               |
                       concrete_format.v
                               |
                               |
                      functional_format.v

---------------------------------------------------------------------

Thanks

The work presented here was started during a stay at SRI/CSL,
Menlo Park. I wish to thank Natarajan Shankar and John Rushby.