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 reports@cs.cmu.edu