A semantical and operational account of call-by-value solvability

Abstract

In Plotkin's call-by-value lambda-calculus, solvable terms are characterized syntactically by means of call-by-name reductions and there is no neat semantical characterization of such terms. Preserving confluence, we extend Plotkin's original reduction without adding extra syntactical constructors, and we get a call-by-value operational characterization of solvable terms. Moreover, we give a semantical characterization of solvable terms in a relational model, based on Linear Logic, satisfying the Taylor expansion formula. As a technical tool, we also use a resource-sensitive calculus (with tests) in which the elements of the model are definable. © 2014 Springer-Verlag.