Jason Reed

A Hybrid Logical Framework Degree Type: Ph.D. in Computer Science
Advisor(s): Frank Pfenning
Graduated: August 2009

Abstract:

The logical framework LF is a constructive type theory of dependent functions that can elegantly encode many other logical systems. Prior work has studied the benefits of extending it to the linear logical framework LLF, for the incorporation linear logic features into the type theory affords good representations of state change. We describe and argue for the usefulness of an extension of LF by features inspired by hybrid logic, which has several benefits. For one, it shows how linear logic features can be decomposed into primitive operations manipulating abstract resource labels. More importantly, it makes it possible to realize a metalogical framework capable of reasoning about stateful deductive systems encoded in the style familiar from prior work with LLF, taking advantage of familiar methodologies used for metatheoretic reasoning in LF.

Thesis Committee:
Frank Pfenning (Chair)
Karl Crary
Robert Harper
Rajeev Goré (Australian National University, Canberra)

Peter Lee, Head, Computer Science Department
Randy Bryant, Dean, School of Computer Science

Keywords:
Automated Reasoning, Logical Frameworks, Linear Logic, Hybrid Logic