Abstract
Call-by-need semantics underlies the widely used programming language Haskell. Unfortunately, unlike call-by-value counterparts, there are no verified compilers for call-by-need. In this paper we present the first verified compiler for call-by-need semantics. We use recent work on a simple call-by-need abstract machine as a way of reducing the formalization burden. We discuss some of the difficulties in verifying call-by-need, and show how we overcome them.
Type
Publication
IFL 2018: Proceedings of the 30th Symposium on Implementation and Application of Functional Languages