Operational Properties of Lily, a Polymorphic Linear Lambda
Calculus with Recursion
G.M.Bierman, A.M. Pitts and C.V.Russo
Abstract
Plotkin has advocated the combination of linear lambda calculus,
polymorphism and fixed point recursion as an expressive semantic
metalanguage. We study its expressive power from an operational point
of view. We show that the naturally call-by-value operators of linear
lambda calculus can be given a call-by-name semantics without
affecting termination at exponential types and hence without
affecting ground contextual equivalence. This result is used to prove
properties of a logical relation that provides a new extensional
characterisation of ground contextual equivalence and relational
parametricity properties of polymorphic types.