A Multiple-Conclusion Meta-Logic
University of Pennsylvania
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, lambda Prolog and its linear logic refinement, Lolli,
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) provides for
concurrency but lacks abstraction mechanisms. In this paper we
present Forum, a logic programming presentation of all of linear logic
that modularly extends the languages 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 non-functional features as
counters and references.
To appear in the Proceedings of LICS'94, Paris. It is also available
via the URL
or via anonymous ftp from
ftp.cis.upenn.edu in the file pub/papers/miller/lics94.dvi.Z
Miller's home page for WWW is http://www.cis.upenn.edu/~dale