A Hybrid Logical Framework

Abstract

The logical framework LF is a constructive type theory of dependent func- tions 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 representa- tions 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 deduc- tive systems encoded in the style familiar from prior work with LLF, taking advantage of familiar methodologies used for metatheoretic reasoning in LF.

Acknowledgments

From the very first computer science course I took at CMU, Frank Pfenning has been an exceptional teacher and mentor. For his patience, breadth of knowledge, and mathematical good taste I am extremely thankful. No less do I owe to the other two major contributors to my programming languages education, Bob Harper and Karl Crary.

Thanks to all the other students, without which grad school wouldn’t be a tenth as fun. Anything I’ve accomplished here is a footnote to time spent over lunches or at the whiteboards with Kevin, Brigitte, Aleks, Kaustuv, Tom, Donna, Spoons, Deepak, William, Chris, Neel, D, Noam, and Dan. Thanks to all of you!

This work is dedicated to my parents — most surely of all I wouldn’t be where I am today without their support and encouragement.

DOWNLOAD...