paper available

To: linear@cs.stanford.edu
Subject: paper available
From: dale@saul.cis.upenn.edu (Dale Miller)
Date: Thu, 28 Apr 94 16:50:42 EDT
Approved: types@dcs.gla.ac.uk




		   A Multiple-Conclusion Meta-Logic

			     Dale Miller
		      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 
       file://ftp.cis.upenn.edu/pub/papers/miller/lics94.dvi.Z
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