Jeff Polakow

Ordered Linear Logic and Applications Degree Type: Ph.D. in Computer Science
Advisor(s): Frank Pfenning, John Reynolds
Graduated: August 2001

Abstract:

This thesis introduces a new logical system, ordered linear logic, which combines reasoning with unrestricted, linear, and ordered hypotheses. The logic conservatively extends (intuitionistic) linear logic, which contains both unrestricted and linear hypotheses, with a notion of ordered hypotheses. Ordered hypotheses must be used exactly once, subject to the order in which they were assumed (i.e., their order cannot be changed during the course of a derivation). This ordering constraint allows for logical representations of simple data structures such as stacks and queues. We construct ordered linear logic in the style of Martin-Lof from the basic notion of a hypothetical judgement. We then show normalization for the system by constructing a sequent calculus presentation and proving cut-elimination of the sequent system.

After introducing the basic logical system, we show how to extend techniques from linear logic to achieve an ordered logic programming language, Olli, and an ordered logical framework, OLF. Olli and OLF allow quite elegant encodings of situations involving simple data structures which are not possible without ordered hypotheses. Example Olli programs include a translator to and from deBruijn notation, and a breadth-first graph traversal program. The major OLF application presented in this dissertation is an analysis of some syntactic properties of the CPS transform.

Thesis Committee:
Frank Pfenning (Chair)
Robert Harper
John Reynolds
Dana Scott
Dale Miller (Pennsylvania State University)

Randy Bryant, Head, Computer Science Department
James Morris, Dean, School of Computer Science

Keywords:
Ordered linear logic, linear logic, non-commututative logic, logic programming, logical frameworks