Linear Logic Programming with Ordered Contexts

Jeff Polakow

To appear at the 2nd International Conference on Principles and Practice of Declarative Programming (PPDP 2000), Montreal, Canada, September 20-22, 2000


We begin with an overview of ordered linear logic (OLL), a refinement of intuitionistic linear logic with an inherent notion of order. We then develop a logic programming interpretation for OLL in two steps: (1) we give a system of ordered uniform derivations which is sound and complete with respect to OLL, 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 with several example programs.