## User login## Navigation |
## Lambda Calculus## On Evaluation Contexts, Continuations, and the Rest of Computation
Although already mentioned before, I believe this paper (which reconciles two approaches to defining continuations) deserves a separate story.
On Evaluation Contexts, Continuations, and the Rest of Computation Continuations are variously understood as representations of the current evaluation context and as representations of the rest of the computation, but these understandings contradict each other: plugging an expression in a context yields a new expression whereas sending an intermediate result to a continuation yields the final answer. We show that continuations-as-evaluation-contexts are the defunctionalized representation of the continuation of a single-step reduction function and that continuations-as-the-rest-of-thecomputation are the continuation of an evaluation function. Furthermore, we show that defunctionalizing the continuation of an evaluator gives rise to the same evaluation contexts as in the single-step reducer. The only difference is how these evaluation contexts are interpreted: a â€˜plugâ€™ interpretation yields one-step reduction, whereas a â€˜refocusâ€™ interpretation yields evaluation. By Andris Birkmanis at 2005-06-08 13:45 | Lambda Calculus | Semantics | 1 comment | other blogs | 5092 reads
## From shift and reset to polarized linear logic
By now, shift/reset should be as popular as call/cc was ten years ago. Some think these control operators are even more important in practice than call/cc, and should be directly supported by PLs. I believe, this paper by Chung-chieh Shan will be interesting to many who loves logic and Curry-Howard isomorphism.
From shift and reset to polarized linear logic Abstract: Griffin pointed out that, just as the pure lambda-calculus corresponds to intuitionistic logic, a lambda-calculus with first-class continuations corresponds to classical logic. We study how first-class delimited continuations, in the form of Danvy and Filinskiâ€™s shift and reset operators, can also be logically interpreted. First, we refine Danvy and Filinskiâ€™s type system for shift and reset to distinguish between pure and impure functions. This refinement not only paves the way for answer type polymorphism, which makes more terms typable, but also helps us invert the continuation-passing-style (CPS) transform: any pure lambda-term with an appropriate type is beta-eta-equivalent to the CPS transform of some shift-reset expression. We conclude that the lambda-calculus with shift and reset and the pure lambda-calculus have the same logical interpretation, namely good old intuitionistic logic. Second, we mix delimited continuations with undelimited ones. Informed by the preceding conclusion, we translate the lambda-calculus with shift and reset into a polarized variant of linear logic that integrates classical and intuitionistic reasoning. Extending previous work on the lambda-Âµ-calculus, this unifying intermediate language expresses computations with and without control effects, on delimited and undelimited continuations, in call-by-value and call-byname settings. By Andris Birkmanis at 2005-06-06 19:17 | Functional | Lambda Calculus | Semantics | Type Theory | 15 comments | other blogs | 9685 reads
## LambdascopeLambdascope:
Remembering our discussion on atoms of PLs (such as scope and name), I decided this paper might be of interest. ## Foundational Calculi for Programming Languages (intro)Since pi calculus is a hot topic lately, Pierce's Foundational Calculi for Programming Languages might be of interest as an introduction. It very briefly introduces and justifies foundational calculi in general, spends about 10 pages on lambda calculus, then builds on that with another 7 pages on pi calculus. By Anton van Straaten at 2005-03-16 08:16 | Lambda Calculus | Parallel/Distributed | login or register to post comments | other blogs | 6303 reads
## A New Approach to Abstract Syntax with Variable BindingPitts and Gabbay, A New Approach to Abstract Syntax with Variable Binding, FAC 2001.
In the lambda calculus, the particular choice of variable names - - as mnemonics to help human readers understand their role, and
- to distinguish variables that are meant to be different and unify variables that are meant to be the same.
In a theory of binders, only the latter purpose is relevant. This is why it's so annoying to have to deal with capture-avoiding substitution, the Barendregt variable convention,
There are several standard ways to deal with this. Generating fresh names with This paper introduces a theory of fresh names that restores algebraic reasoning, referential transparency, and structural induction to algebraic datatypes with a HOAS-like notation for introducing binders into an abstract syntax. This is the set-theoretical basis for the authors' work on FreshML and FreshO'Caml, which we've discussed a little bit on LtU in the past. By Dave Herman at 2005-03-14 15:53 | Lambda Calculus | Meta-Programming | Theory | 7 comments | other blogs | 8052 reads
## Barbara Partee: Reflections of a Formal Semanticist as of Feb 2005What follows will be a very subjective and personal view, as much my own history and development in the field and how things looked through my eyes as about the development of the field itself. This essay is about natural language semantics, but you'll find old friends here: lambdas, bindings, types, quantifiers etc. If you are lazy, go directly to footnote 25... No surprise, really, if you follow the links we give here from time to time about TLGs and such. By Ehud Lamm at 2005-02-15 10:37 | History | Lambda Calculus | Semantics | Type Theory | 5 comments | other blogs | 9346 reads
## The Church Project
http://types.bu.edu or http://www.church-project.org
We previously linked to a document on this site, but not the site itself. By Andris Birkmanis at 2005-02-08 17:24 | Lambda Calculus | Type Theory | 3 comments | other blogs | 4984 reads
## The pi-Calculus in Direct StyleThe pi-Calculus in Direct Style
a.k.a. Blue Calculus ## Normal-order direct-style beta-evaluator with syntax-rules, and the repeated applications of call/cc
Oleg's presentation at the workshop in honor of Daniel Friedman is great fun as usual.
The topic of repeated applications of call/cc has been mentioned on LtU previously, a few years
ago. New this time: the full and correct beta-normalizer written as a
direct-style syntax-rule. The normalizer implements calculus of
explicit substitutions. The talk presents probably the shortest (and
the fastest) normal-order beta-normalizer as a (stand-alone) Scheme
macro. Another new feature is the discussion of self-applications of
delimited continuation operators. The talk mentions incidentally that
shift, control, shift0 and other, less-delimited control operators are the members of the same family: gshift/greset.
Hot stuff. By Ehud Lamm at 2005-01-19 13:07 | Lambda Calculus | Meta-Programming | Semantics | 1 comment | other blogs | 6887 reads
## Call-by-Name, Call-by Value and the Lambda Calculus
Gordon Plotkin's
Call-by-Name, Call-by-Value and the Lambda Calculus (Theoretical Computer Science , Vol. 1, pp. 125-159, 1975), is available online.
The fundamental point made in the paper should seem natural to most LtU readers: In order to reason about programming language semantics one should look for programming language/calculus The paper contrasts CBN and CBV, and shows the differences between the Lambda Calculi appropriate for describing each of them. |
## Browse archives## Active forum topics |

## Recent comments

1 day 6 hours ago

1 day 11 hours ago

2 days 11 hours ago

2 days 13 hours ago

2 days 19 hours ago

3 days 12 hours ago

3 days 21 hours ago

4 days 8 hours ago

4 days 9 hours ago

4 days 9 hours ago