The [lambda]-calculus provides a simple, well-established framework for research in functional programming languages that readily lends itself to the use offormal methods--that is, the use of mathematically sound techniques ...