Forum: A Multiple Conclusion Specification Logic

Description

Niveau: Supérieur
Forum: A Multiple-Conclusion Specification Logic Dale Miller Computer Science Department University of Pennsylvania Philadelphia, PA 19104-6389 USA Draft: January 3, 1996 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 [15], provide for various forms of abstraction (modules, abstract data types, and higher-order programming) but lack primitives for concurrency. The logic programming language, LO (Lin- ear Objects) [2] provides some primitives for concurrency but lacks abstraction mechanisms. In this paper we present Forum, a logic programming presenta- tion of all of linear logic that modularly extends ?Prolog, Lolli, and LO. Forum, therefore, allows specifications to incorporate both abstractions and concur- rency. To illustrate the new expressive strengths of Forum, we specify in it a sequent calculus proof system and the operational semantics of a program- ming language that incorporates references and concurrency. We also show that the meta theory of linear logic can be used to prove properties of the object- languages specified in Forum. This paper will appear in Theoretical Computer Science. 1

• contain right-introduction rules


• conclusion sequents


• linear logic


• logic connectives


• logic programming


• cut-elimination theorem


• logical constants


• sequent calculus

Sujets

• Linear logic
• Logic programming
• Cut-elimination theorem
• Logical constant
• Sequent calculus

Informations

• Publié par: chaeh
• Nombre de lectures: 19
• Langue: English

Extrait

A

Forum:

Multiple-Conclusion

Specication Logic

Dale Miller Computer Science Department University of Pennsylvania Philadelphia, PA 19104-6389 USA [e-mail] http://www.cis.upenn.edu/∼dale

Draft: January 3, 1996

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 renement, Lolli [15], provide for various forms of abstraction (modules, abstract data types, and higher-order programming) but lack primitives for concurrency. The logic programming language, LO (Lin- ear Objects) [2] provides some primitives for concurrency but lacks abstraction mechanisms. In this paper we present Forum, a logic programming presenta- tion of all of linear logic that modularly extendsλProlog, Lolli, and LO. Forum, therefore, allows specications to incorporate both abstractions and concur- rency. To illustrate the new expressive strengths of Forum, we specify in it a sequent calculus proof system and the operational semantics of a program- ming language that incorporates references and concurrency. We also show that the meta theory of linear logic can be used to prove properties of the object- languages specied in Forum.

This paper will appear inTheoretical Computer Science.

1