Paper: A multiple-conclusion meta-logic (at LICS 1994)

Authors: Dale A. Miller

Abstract

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 (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 λ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

BibTeX

  @InProceedings{Miller-Amultipleconclusion,
    author = 	 {Dale A. Miller},
    title = 	 {A multiple-conclusion meta-logic},
    booktitle =  {Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science (LICS 1994)},
    year =	 {1994},
    month =	 {July}, 
    pages =      {272--281},
    location =   {Paris, France}, 
    publisher =	 {IEEE Computer Society Press}
  }