[Prev][Next][Index][Thread]
From Algol to Polymorphic Linear Lambda-calculus
The following manuscript can be found on
http://www.dcs.qmw.ac.uk/~ohearn/
----------------------------------
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.