ACM/IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Ninth Annual IEEE Symposium on

Logic in Computer Science (LICS 1994)

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

Winner of the Test-of-Time Award in 2014
Authors: Dale A. Miller


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


    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}

Last modified: 2022-10-3113:49
Sam Staton