Projects per year

## Abstract

We study beta-reduction in a linear lambda-calculus derived from Abramsky's linear combinatory algebras. Reductions are classified depending on whether the redex is in the computationally active part of a term ("surface" reductions) or whether it is suspended within the body of a thunk ("internal" reductions). If surface reduction is considered on its own then any normalizing term is strongly normalizing. More generally, if a term can be reduced to surface normal form by a combined sequence of surface and internal reductions then every combined reduction sequence from the term contains only finitely many surface reductions. We apply these results to the operational semantics of Lily, a second-order linear lambda-calculus with recursion, introduced by Bierman, Pitts and Russo, for which we give simple proofs that call-by-value, call-by-name and call-by-need contextual equivalences coincide.

Original language | English |
---|---|

Title of host publication | Term Rewriting and Applications |

Subtitle of host publication | 16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005. Proceedings |

Publisher | Springer-Verlag GmbH |

Pages | 219-234 |

Number of pages | 15 |

ISBN (Print) | 978-3-540-25596-3 |

DOIs | |

Publication status | Published - 2005 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer Berlin / Heidelberg |

Volume | 3467 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

## Fingerprint

Dive into the research topics of 'Reduction in a linear lambda-calculus with applications to operational semantics'. Together they form a unique fingerprint.## Projects

- 2 Finished