BRICS · Contents · Programme · References · Prerequisites · Participants · Lecture Notes · Registration

**A BRICS Mini-Course**

**October 27, 1996**

**Lectures by
Kristoffer Høgsbro Rose
**

**
**

The mini-course is five 45-minute lectures that can be attended by everyone; the situation the day before the Verification '96 autumn school makes combination possible.

### Sunday October 27, 1996, 10:15-11:00 in Auditorium D4

**1. Explicit Substitution Rules**The basics of making the lambda-calculus

*operational*by defining substitution as a stepwise primitive operation. We discuss the problems this presents, in particular the danger of introducing*too many*steps such that, for example, simply typed terms are no longer normalising: we show how one proves that an explicit substitution calculus has*PSN*(preserves strong normalisation of beta-reduction).### Sunday October 27, 1996, 11:15-12:00 in Auditorium D4

**2. Explicit Binding**In recent years a large number of ``explicit substitution calculi'' have been proposed that only vary in the representation of

*variable binding*: lambda\*u**p**s**i**l**o**n*, lambda\*c**h**i*, lambda*s*, lambda*t*, and lambdax. We show that these calculi all have essentially the*same reductions*, in particular the renaming overhead is negligible with respect to normalisation.### Sunday October 27, 1996, 12:15-13:00 in Auditorium D4

**3. Explicit Addresses**One of the most intriguing problems in using lambda calculus as a computational model is how to capture

*memory*. We discuss one technique for doing this, an*address oracle*based on the so-called lambda-graph rewriting of Wadsworth. It turns out that the techniques combine well with explicit substitution to form computational models that can be used to measure not only time but also space behaviour of lambda-reduction.### Sunday October 27, 1996, 15:15-16:00 in Auditorium D4

**4. Strategies and Abstract Machines**We explain how explicit substitution provides a technique for separating the issues of

*primitives*and*reduction strategies*, and show how an explicit substitution calculus equipped with a strategy can be used to derive an abstract machine. We exploit the techniques of all the previous chapters to give formally understandable justifications for the techniques used for*sharing*,*recursion*, and*parallelism*, in ``real'' implementations of functional programming languages.### Sunday October 27, 1996, 16:15-17:00 in Auditorium D4

**5. Generalising to Higher-Order Rewriting**We explain how explicit substitution can be used to facilitate reasoning about higher-order rewriting, both by translating higher-order rewrite systems into explicit substitution as well as defining higher-order rewriting through explicit substitution. A few additional complications are encountered when modeling addresses which lead to the notion of

*explicit recursion*.

- M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy, Explicit
substitutions,
*Journal of Functional Programming*, 1(4): 375-416, 1991. - H. Barendregt, The lambda calculus: its syntax and semantics (revised edition), North-Holland, 1984.
- Z.-E.-A. Benaissa, K. H. Rose, and P. Lescanne, Modeling sharing and
recursion for weak reduction strategies using explicit substitution,
*in*H. Kuchen and D. Swierstra (editors),*8th PLILP-Symposium on Programming Language Implementation and Logic Programming*, Aachen, Germany, pp. 393-407, September 1996. - R. Bloo and K. H. Rose, Combinatory reduction systems with explicit
substitution that preserve strong normalisation,
*in*H. Ganzinger (editor),*7th RTA-International Conference on Rewriting Techniques and Applications*, Rutgers University, New Jersey, pp. 169-183, July 1996. - R. Bloo and K. H. Rose, Preservation of strong normalisation in named
lambda calculi with explicit substitution and garbage collection,
*in**CSN '95-Computer Science in the Netherlands*, Koninklijke Jaarbeurs, Utrecht, pp. 62-72, November 1995. - P.-A. Melliès, Typed lambda-calculi with explicit substitution may
not terminate,
*in*M. Dezani, editor,*2nd TLCA-International Conference on Typed Lambda Calculi and Applications*, Edinburgh, Scotland, LNCS 902, pp. 328-334, 1995.## Prerequisites

Knowledge of lambda-calculus [2] as well as some knowledge of the most basic rewriting techniques is assumed (the lecture notes include a summary of the notions and notations actually used).

## Participants

Olivier Danvy <danvy@brics.dk>

Stefan Dziembowski <stefand@mimuw.edu.pl>

Andy Gordon <adg@cl.cam.ac.uk>

Hanne Gottliebsen <hago@daimi.au.dk>

Øystein Haugen <oystein.haugen@nr.no>

Philipp Heuberger <pheuberg@ra.abo.fi>

Thomas Hildebrandt <hilde@brics.dk>

Marcin Jurdzinski <mju@mimuw.edu.pl>

Søren B. Lassen <thales@brics.dk>

Karoline Malmkjær <karoline@stibo.dk>

Randy Pollack <rap@dcs.ed.ac.uk>

Kim Sunesen <ksunesen@brics.dk>

Svend Haugaard Sørensen <shs@daimi.aau>.dk## Lecture Notes

BRICS-LS-96-3## Registration

Please send an E-mail message to \href{mailto:krisrose@brics.dk}{krisrose@brics.dk} if you wish to participate. There is no fee.