21/12/2006
François-Régis Sinot (Universidade do Porto)
More laziness !

Launchbury's natural semantics is a tool of choice to reason about call-by-need evaluation. However, modern non-strict functional languages do not use plain call-by-need evaluation: they also use static optimisations like fully lazy lambda-lifting or partial evaluation. To ease reasoning, it would be nice to have all this in a uniform setting. In this talk, we generalise Launchbury's semantics in order to capture more laziness. More precisely, we capture “complete laziness”, as coined by Holst and Gomard in 1991, which is slightly more than fully lazy sharing, and closer to on-the-fly needed partial evaluation. We discuss the connections between this and other related concepts, like optimal reduction.