From Algol to polymorphic linear lambda-calculus

In a linearly-typed functional language, one can define functions that cons ume their arguments in the process of computing their results. This is remi niscent of state transformations in imperative languages, where execution o f an assignment statement alters the contents of the store. We explore this connection by translating two variations on Algol 60 into a purely functio nal language with polymorphic linear types. On the one hand, the translatio ns 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.