Explicit Substitution - Tutorial & Survey

Kristoffer H. Rose

September 1996

Abstract:

These lecture notes are from the BRICS mini-course ``Explicit Substitution'' taught at University of Aarhus, October 27, 1996.

We give a coherent overview of the area of explicit substitution and some applications. The focus is on the operational or syntactic side of things, in particular we will not cover the areas of semantics and type systems for explicit substitution calculi. Emphasis is put on providing a universal understanding of the very different techniques used by various authors in the area.

Contents

1

Explicit Substitution Rules

1.1

Explicit Substitution

1.2

Preservation of Strong Normalisation (PSN)

1.3

Discussion

2

Explicit Binding

2.1

Namefree -Calculus

2.2

Explicit Binding Variations for Explicit Substitution

2.3

Discussion

3

Explicit Addresses

3.1

-graphs and Explicit Sharing

3.2

Explicit Substitution & Sharing

3.3

Discussion

4

Higher-Order Rewriting and Functional Programs

4.1

Combinatory Reduction Systems (CRS)

4.2

Explicit Substitutes

4.3

Explicit Addresses

4.4

CRS and Functional Programs

4.5

Discussion

5

Strategies and Abstract Machines

5.1

Strategies for -Calculus

5.2

Calculi for Weak Reduction with Sharing

5.3

Reduction Strategies

5.4

Constructors and Recursion

5.5

A Space Leak Free Calculus

5.6

Discussion

A

Appendices: Preliminaries

A.1

Reductions

A.2

Inductive Notations

A.3

-Calculus

Available as PDF, PostScript, PostScript.2up (two pages per A4 landscape sheet).
Errata to printed version (already applied to PostScript version): PostScript, PostScript.2up.
Selected slides (of the five lectures presented on October 27, 1996): 1, 2, 3, 4, 5.