A Multiple-Conclusion Meta-Logic

9 years 6 months ago
A Multiple-Conclusion Meta-Logic
The theory of cut-free sequent proofs has been used to motivate and justify the design of a number of logic programming languages. Two such languages, Prolog and its linear logic refinement, Lolli [12], provide for various forms of abstraction (modules, abstract data types, higher-order programming) but lack primitives for concurrency. The logic programming language, LO (Linear Objects) [2] provides for conbut lacks abstraction mechanisms. In this paper we present Forum, a logic programming presentation of all of linear logic that modularly extends the languages Prolog, Lolli, and LO. Forum, therefore, allows specifications to incorporate both abstractions and concurrency. As a meta-language, Forum greatly extends the expressiveness of these other logic programming languages. To illustrate its expressive strength, we specify in Forum a sequent calculus proof system and the operational semantics of a functional programming language that incorporates such nonfunctional features as count...
Dale Miller
Added 09 Aug 2010
Updated 09 Aug 2010
Type Conference
Year 1994
Where LICS
Authors Dale Miller
Comments (0)