Functional Programming Languages with Logical Variables: A Linear Logic View

The idea of introducing logical variables into functional programming languages has been proposed for some years, and many concrete languages with this feature have been developed. Recently the semantic features of the languages in this paradigm have been uniformly modelled using the constraint computation formalism [RJK92]. However, the operational behaviour of these languages has not been studied systematically. In this paper, we propose a linear logic formalization of the the computational behaviour of functional programming languages with logical variables. It is shown that, with the resource-consciousness of linear logic, the computation of the paradigm can be uniformly modelled as deduction in the logic. Therefore, the model provides the logical meaning for the computation as well as a general abstract machine for the implementation of these languages