CMU-CS-01-152Computer Science Department School of Computer Science, Carnegie Mellon University
CMU-CS-01-152
Jeff Polakow August 2001 Ph.D. Thesis
CMU-CS-01-152.ps
Keywords: Ordered linear logic, linear logic, non-commututative
logic, logic programming, logical frameworks
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 This page maintained by reports@cs.cmu.edu |