From Algol to polymorphic linear lambda-calculus

In a linearly-typed functional language, one can define functions that consume their arguments in the process of computing their results. This is reminiscent of state transformations in imperative languages, where execution of an assignment statement alters the contents of the store. We explore this connection by translating two variations on Algol 60 into a purely functional language with polymorphic linear types. On the one hand, the translations lead to a semantic analysis of Algol-like programs, in terms of a model of the linear language. On the other hand, they demonstrate that a linearly-typed functional language can be at least as expressive as Algol.