User loginNavigation 
Lambda CalculusFrom 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 Chungchieh Shan will be interesting to many who loves logic and CurryHoward isomorphism.
From shift and reset to polarized linear logic Abstract: Griffin pointed out that, just as the pure lambdacalculus corresponds to intuitionistic logic, a lambdacalculus with firstclass continuations corresponds to classical logic. We study how firstclass 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 continuationpassingstyle (CPS) transform: any pure lambdaterm with an appropriate type is betaetaequivalent to the CPS transform of some shiftreset expression. We conclude that the lambdacalculus with shift and reset and the pure lambdacalculus 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 lambdacalculus 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 callbyvalue and callbyname settings. By Andris Birkmanis at 20050606 19:17  Functional  Lambda Calculus  Semantics  Type Theory  15 comments  other blogs  8960 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 20050316 08:16  Lambda Calculus  Parallel/Distributed  login or register to post comments  other blogs  6045 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  even free variables  is irrelevant. Names serve two purposes:
In a theory of binders, only the latter purpose is relevant. This is why it's so annoying to have to deal with captureavoiding 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 HOASlike notation for introducing binders into an abstract syntax. This is the settheoretical 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 20050314 15:53  Lambda Calculus  MetaProgramming  Theory  7 comments  other blogs  7561 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 20050215 10:37  History  Lambda Calculus  Semantics  Type Theory  5 comments  other blogs  8925 reads
The Church Project
http://types.bu.edu or http://www.churchproject.org
We previously linked to a document on this site, but not the site itself. By Andris Birkmanis at 20050208 17:24  Lambda Calculus  Type Theory  3 comments  other blogs  4686 reads
The piCalculus in Direct StyleThe piCalculus in Direct Style
a.k.a. Blue Calculus Normalorder directstyle betaevaluator with syntaxrules, 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 betanormalizer written as a
directstyle syntaxrule. The normalizer implements calculus of
explicit substitutions. The talk presents probably the shortest (and
the fastest) normalorder betanormalizer as a (standalone) Scheme
macro. Another new feature is the discussion of selfapplications of
delimited continuation operators. The talk mentions incidentally that
shift, control, shift0 and other, lessdelimited control operators are the members of the same family: gshift/greset.
Hot stuff. By Ehud Lamm at 20050119 13:07  Lambda Calculus  MetaProgramming  Semantics  1 comment  other blogs  6550 reads
CallbyName, Callby Value and the Lambda Calculus
Gordon Plotkin's
CallbyName, CallbyValue and the Lambda Calculus (Theoretical Computer Science , Vol. 1, pp. 125159, 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 pairs. The paper contrasts CBN and CBV, and shows the differences between the Lambda Calculi appropriate for describing each of them. Theoretical Pearl: Church numerals, twice!
Ralf Hinze. Theoretical Pearl: Church numerals, twice! Journal of Functional Programming, 2004. To appear.
This pearl explains Church numerals, twice. The first explanation links Church numerals to Peano numerals via the wellknown encoding of data types in the polymorphic LC. This view suggests that Church numerals are folds in disguise. The second explanation, which is more elaborate, but also more insightful, derives Church numerals from first principles, that is, from an algebraic specification of addition and multiplication. Additionally, we illustrate the use of the parametricity theorem by proving exponentiation as reverse application correct. A simple concept is used to demonstrate several interesting and useful techniques. By Ehud Lamm at 20040715 13:27  Lambda Calculus  login or register to post comments  other blogs  4109 reads

Browse archivesActive forum topics 
Recent comments
9 hours 52 min ago
11 hours 34 min ago
18 hours 19 min ago
20 hours 31 min ago
22 hours 5 sec ago
22 hours 44 min ago
1 day 3 hours ago
1 day 10 hours ago
1 day 10 hours ago
1 day 11 hours ago