SCS Undergraduate Thesis Topics
|Chris Martens||Frank Pfenning||A Hybrid Formulation of the Ordered Logical Framework|
The logical framework LF is a powerful tool for encoding and carrying out the metatheory of logics and programming languages in a mechanized way. However, current work on LF has yielded little support for the metatheory of certain kinds of logic that are useful for reasoning about state. One fruitful approach (for the case of linear logic) has been to use hybrid logic, inspired by Kripke modal logic and temporal logic, to give the metareasoning tool access to how the object language context is being manipulated. The goal of this thesis is to apply the same approach to ordered logic, an setting capable of expressing even more constraints.