Single-threaded polymorphic lambda calculus

The primary goal of this study is to devise a method to express mutations to state in a modern (higher order, polymorphic, nonstrict) functional language, without sacrificing referential transparency, and with a simple, easy-to-reason-about semantics. Although collectively these properties seem contradictory, a satisfactory solution is found. Aside from the fundamental property of referential transparency, the two key properties that the authors maximize are simplicity and expressiveness. The system must be easy to use: expressing mutations to state should be natural, and the resulting behavior should be easy to reason about