Pitts 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 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.
What 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.
http://types.bu.edu or http://www.church-project.org
We previously linked to a document on this site, but not the site itself.
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.
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 pairs.
The paper contrasts CBN and CBV, and shows the differences between the Lambda Calculi appropriate for describing each of them.
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 well-known 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.
Henk Barendregt needs no introduction for many LtU readers - he literally wrote "the book" on the lambda calculus, and that only hints at the profound impact his work has had on lambda calculus and type theory.
The page linked above lists two overlapping papers, both about reflection:
As the first paragraph quoted above implies, the scope of these two papers extends far beyond the lambda calculus, into fields such as biology and meditation. Between the two papers, there's something for everyone:
"Reflection and its use, from science to meditation" is wide-ranging, covering reflection related to living cells, formal languages, mathematics, art, computers, and the human mind.
"Reflection and its use, with an emphasis on languages and lambda calculus", focuses specifically on reflection in formal languages, including combinatory logic and lambda calculus.
Active forum topics
New forum topics