A multiple-conclusion meta-logic
Dale Armin Miller · 2002
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, /spl lambda/Prolog and its linear logic refinement, Lolli (J. Hodas and D. Miller, 1994), 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) (J. Andreoli and R. Pareschi, 1991) provides for concurrency but lacks abstraction mechanisms. We present Forum, a logic programming presentation of all of linear logic that modularly extends the languages /spl lambda/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 counters and references.>