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.

277 pages

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

This page maintained by reports@cs.cmu.edu