Abstract:
We present the 
-calculus, a formal
synthesis of the concepts of sharing and explicit substitution for weak
reduction. We show how can be used as a foundation of
implementations of functional programming languages by modeling the essential
ingredients of such implementations, namely weak reduction strategies,
recursion, space leaks, recursive data structures, and
parallel evaluation, in a uniform way.
First, we give a precise
account of the major reduction strategies used in functional programming and
the consequences of choosing 
-graph-reduction vs. environment-based
evaluation. Second, we show how to add constructors and explicit
recursion to give a precise account of recursive functions and data
structures even with respect to space complexity. Third, we formalize the
notion of space leaks in and use this to define a
space leak free calculus; this suggests optimisations for call-by-need
reduction that prevent space leaking and enables us to prove that the
``trimming'' performed by the STG machine does not leak space.
In summary we give a formal account of several implementation techniques used by state of the art implementations of functional programming languages
Available as PostScript, PDF.