## You are here

# Standardisation in Rewriting

**Abstract**

*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 *d*. The “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).

**Prerequisites:**