Minimal thunkification

Abstract

By “thunkifying” the arguments to function applications and “dethunkifying” variables one can translate a λ-expression e into a λ-expression e', such that call-by-value evaluation of e’ gives the same result as call-by-name evaluation of e. By using the result of a strictness analysis, some of these thunkifications can be avoided. In this paper we present a type system for strictness analysis; present a translation algorithm which exploits the strictness proof tree; and give a combined proof of the correctness of the analysis/translation.