You are here

Standardisation in Rewriting


Lecturer: Eduardo Bonelli, Universidad de Quilmes, Argentina

Given a derivation d from a source term s to a target term t in lambda calculus or a TRS, consider the reduction space obtained from all the derivations which result from permuting steps in dThe “standardisation theorem” states that in this reduction space one may always single out a (unique) derivation, the standard derivation. This tutorial introduces the notion of “standard” derivation both in lambda calculus and TRS starting from the theory of residuals on which it stands. We review alternative definitions and then explore the applications of the standardisation theorem in the foundations of programming languages including normalisation of reduction strategies and correspondence between calculi for reasoning about programming languages and their implementation (Plotkin).


Basic knowledge of lambda calculus and term rewriting systems (TRS). 
Material for this presentation can be found here.
Excercises can be found here.