| Abstract |
Bibliography |
The Virtues of Eta-Expansion
Abstract
Authors CBJ and N. Ghani
Interpreting eta-conversion as an expansion rule in the simply-typed
lambda-calculus maintains the confluence of reduction in a richer type
structure. This use of expansions is supported by categorical models
of reduction, where beta-contraction, as the local counit, and
eta-expansion, as the local unit, are linked by local triangle
laws. The latter form reduction loops, but strong normalisation (to
the long beta/eta-normal forms) can be recovered by ``cutting'' the
loops.
Page Last Updated:
Main |
Personal Details |
Research Interests |
Research Publications
FISh |
SDCS |
Site Map
Please feel free to send any comments.
Copyright Barry Jay © 1998
