The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT imag.fr>]

You may have a look in the contribs from Lannion about exceptions,
and my related paper in SCP.

In summary, it is a kind of CPS translation where the result and its
type need to be local (rather than global as usual). In particular,
for ensuring modularity: a function raising an exception has a meaning
indepandantly from its context. When a recursive call is embedded
inside a "try with" construct, impredicativity comes naturally into
play.

The contrib uses impredicative Set.

@article{jfm-scp-96,
  author = {J-F. Monin},
  title = {{Exceptions considered harmless}},
  journal = {{Science of Computer Programming}},
  ps = {http://www-verimag.imag.fr/~monin/Publis/scp96.ps},
  pdf = {http://www-verimag.imag.fr/~monin/Publis/scp96.pdf},
  abstract = {Program extraction is a well known technique for
              developing correct functional programs from a
              constructive proof of their specification.  This paper
              shows how to deal with exceptions in such a framework.
              We propose a modular (and impredicative) formalization
              in the calculus of constructions and we illustrate the
              technique on three examples.},
  year = 1996,
  volume = 26,
  pages = {179--196}
}


On Sat, Aug 27, 2011 at 08:20:38AM -0400, Adam Chlipala wrote:
> Even without such an axiom, it already has a richer notion than in
> [Set], because [Prop] allows impredicativity, but my suspicion is
> that few proofs make deep use of impredicativity.  (Does anyone have
> a non-contrived counterexample to that suspicion?)
> 
> 

-- 
Jean-Francois Monin
LIAMA Project FORMES, CNRS  &  Universite de Grenoble 1

Office 3-605, FIT, Tsinghua University
Haidian District, Beijing 100084, CHINA
Tel: +86 10 62 79 69 79 ext 605
Fax@LIAMA:
 +86 10 6264 7458