coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] I am cautious about adding some axioms, ±èÇü¼±
- Re: [Coq-Club] I am cautious about adding some axioms,
Pierre-Marie Pedrot
- Re: [Coq-Club] I am cautious about adding some axioms,
Adam Chlipala
- Re: [Coq-Club] I am cautious about adding some axioms, Jean-Francois Monin
- Re: [Coq-Club] I am cautious about adding some axioms, Adam Chlipala
- Re: [Coq-Club] I am cautious about adding some axioms, Jean-Francois Monin
- Re: [Coq-Club] I am cautious about adding some axioms, AUGER Cedric
- Re: [Coq-Club] I am cautious about adding some axioms,
Adam Chlipala
- Re: [Coq-Club] I am cautious about adding some axioms, Adam Chlipala
- Re: [Coq-Club] I am cautious about adding some axioms,
Pierre-Marie Pedrot
Archive powered by MhonArc 2.6.16.