Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] I am cautious about adding some axioms

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] I am cautious about adding some axioms


chronological Thread 
  • From: Jean-Francois Monin <jean-francois.monin AT imag.fr>
  • To: Adam Chlipala <adamc AT csail.mit.edu>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] I am cautious about adding some axioms
  • Date: Tue, 30 Aug 2011 15:35:03 +0800

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



Archive powered by MhonArc 2.6.16.

Top of Page