Timeline for What fails when using call/cc as realizer of the Peirce formula
Current License: CC BY-SA 2.5
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 17, 2011 at 14:48 | comment | added | Finn Lawler | Yes, you're quite right. Fixed. | |
| Jan 17, 2011 at 14:47 | history | edited | Finn Lawler | CC BY-SA 2.5 |
deleted 4 characters in body
|
| Jan 17, 2011 at 5:44 | comment | added | Daniel Mehkeri | I think it's the other way around: to implement LEM, initially take the negative disjunct and pretend to be a proof of not-A, that is, a function taking as paramter a proof of A and returning a proof of contradiction. If the function is invoked with an actual proof of A as an argument, instead of returning a contradiction (which is impossible) go "back in time" and take the positive disjunct, returning the given proof of A... | |
| Jan 16, 2011 at 19:31 | comment | added | Finn Lawler | That's Philip Wadler, Call-by-value is dual to call-by-name and Franco Barbanera & Stefano Berardi (look here: informatik.uni-trier.de/~ley/db/indices/a-tree/b/…). Or have a look at my TCD technical report (not peer-reviewed) here: cs.tcd.ie/publications/tech-reports/reports.08/… | |
| Jan 16, 2011 at 19:08 | comment | added | Christoph-Simon Senjak | Thank you for your answer. So far I was only concerned with program extraction from intuitionistic proofs. Wadler = Philip Wadler? If so, there are a lot of papers of him, could you get more specific? For Franco(?) Barbanera I do not really find much that seems to be related. And there are a lot of people called Berardi, do you have a prename? | |
| Jan 16, 2011 at 18:58 | vote | accept | Christoph-Simon Senjak | ||
| Jan 16, 2011 at 16:38 | history | answered | Finn Lawler | CC BY-SA 2.5 |