Computer Science Department
School of Computer Science, Carnegie Mellon University


Ordered Linear Logic Programming

Jeff Polakow, Frank Pfenning

December 1998


Keywords: Intuitionistic non-commutative linear logic, linear logic programming

We begin with a review of intuitionistic non-commutative linear logic (INCLL), a refinement of linear logic with an inherent notion of order proposed by the authors in prior work. We then develop a logic programming interpretation for INCLL in two steps: (1) we give a system of ordered uniform derivations which is sound and complete with respect to INCLL, and (2) we present a model of resource consumption which removes non-determinism from ordered resource allocation during search for uniform derivations. We also illustrate the expressive power of the resulting ordered linear logic programming language through some examples, including programs for merge sort, insertion sort, and natural language parsing.

33 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by