From Algol to Polymorphic Linear Lambda-calculus

We translate two variations on Algol 60 into the polymorphic linear lambda-calculus, extended with a fixed-point operator. One of the translations is for a version of Idealized Algol with side effects in expressions, and the other is for Idealized Algol under the syntactic control of interference discipline. Parametric polymorphism in the target language is used to explicate noninterference and local state in the source languages, while linearity (combined with polymorphism) is used to explicate irreversibility of state change. The use of the translations in showing various program equivalences is demonstrated by considering a a semantic model of the target language based on a strict function version of relational parametricity, and an explicit description of the structure of first order types is given. 1 Introduction Imperative languages have a dynamic character that is not captured well using just the traditional domain-theoretic methods of denotational semantics. Traditional semant..