A Hybrid Logical Framework

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 front prior work with LLF, taking advantage of familiar methodologies used for metatheoretic reasoning in LF.