From Algol to Polymorphic Linear Lambda-calculus

The following manuscript can be found on 


 From Algol to Polymorphic Linear Lambda-calculus
 Peter W. O'Hearn and John C. Reynolds

In a linearly-typed functional language one can define functions
that consume their arguments in the process of computing their results.
This is reminiscient 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 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.