Proving the Correctness of the STG Machine

Abstract. J. Launchbury gave an operational semantics for lazy evaluation and showed that it is sound and complete w.r.t. a denotational s of the language. P. Sestoft then introduced several abstract machines for lazy evaluation and showed that they were sound and complete w.r.t. Launchbury’s operational semantics. We go a step forward and show that the Spineless Tagless G-machine is complete and (almost) sound w.r.t. one of Sestoft’s machines. In the way to this goal we also prove some interesting properties about the operational semantics and about Sestoft’s machines which clarify some minor points on garbage collection and on closures’ local environments. Unboxed values and primitive operators are excluded from the study.

• Type: Conference
• Year: 2001
• Where: IFL
• Authors: Alberto de la Encina, Ricardo Pena
• Keywords: Complete W.r.t, Formal Methods, IFL 2001, Lazy Evaluation, Operational Semantics