Closures and Modules Within Linear Logic Concurrent Constraint Programming
There are two somewhat contradictory ways of looking at modules in a given programming language. On the one hand, module systems are largely independent of the particulars of programming languages. On the other hand, the module constructs may interfere wi
- PDF / 488,583 Bytes
- 13 Pages / 430 x 660 pts Page_size
- 5 Downloads / 223 Views
tract. There are two somewhat contradictory ways of looking at modules in a given programming language. On the one hand, module systems are largely independent of the particulars of programming languages. On the other hand, the module constructs may interfere with the programming constructs, and may be redundant with the other scope mechanisms of a specific programming language, such as closures for instance. There is therefore a need to unify the programming concepts that are similar, and retain a minimum number of essential constructs to avoid arbitrary programming choices. In this paper, we realize this aim in the framework of linear logic concurrent constraint programming (LCC) languages. We first show how declarations and closures can be internalized as agents in a variant of LCC for which we provide precise operational and logical semantics in linear logic. Then, we show how a complete module system can be represented within LCC, and prove for it a general code protection property. Finally we study the instanciation of this scheme to the implementation of a safe module system for constraint logic programs, and conclude on the generality of this approach to programming languages with logical variables.
1
Introduction
Module systems are an essential feature of programming languages as they facilitate the re-use of existing code and the development of general purpose libraries. There are however two contradictory ways of looking at a module system. On the one hand, a module system is essentially independent of the particulars of a given programming language. “Modular” module systems have thus been designed and indeed adapted to different programming languages, see e.g. [15]. On the other hand, module constructs often interfere with the programming constructs and may be redundant with other scope mechanisms supported by a given programming language, such as closures for instance. There is therefore a need to unify the programming concepts that are similar in order to retain a minimum number of essential constructs and avoid arbitrary programming choices. In this paper, we realize this aim in the framework of linear logic concurrent constraint (LCC) programming languages. The class of concurrent constraint (CC) programming languages was introduced in [18] as an elegant merge of constraint logic programming (CLP) and V. Arvind and S. Prasad (Eds.): FSTTCS 2007, LNCS 4855, pp. 544–556, 2007. c Springer-Verlag Berlin Heidelberg 2007
Closures and Modules Within Linear LCC Programming
545
concurrent logic programming. In the CC paradigm, CLP goals become concurrent agents communicating through a common store of constraints, each agent being able to post constraints to the store, and to synchronize by asking whether a guard constraint is entailed by the store. Research on the logical semantics of CC languages [6] led to a simple solution in Girard’s Linear Logic [8]. Through a straightforward translation of CC agents into intuitionistic LL (ILL) formulas, CC operational transitions indeed correspond to deductions in
Data Loading...
