Colloquium Details
From classical logic to delimited control in the hierarchy, via separation
| Author: | Alexis Saurin INRIA pi.r2 |
|---|---|
| Date: | March 04, 2010 |
| Time: | 15:30 |
| Location: | 220 Deschutes |
| Host: | Zena Ariola |
Abstract
I shall first review results on extensions of the Proof-Program correspondence (a.k.a Curry-Howard correspondence) to classical logic in the line of Parigot's early 90's work on lambda-mu-calculus, focusing in particular on the separation property. Then, I shall introduce a slight extension of lambda-mu which completes Parigot's calculus (in the sense of Böhm completeness) and then lift this to a hierarchy of calculi that I will show to correspond to Danvy and Filinksi's CPS hierarchy of delimited control operator via the call-by-name/call-by-value duality.