Hybridizing a Logical Framework

Logical connectives familiar from the study of hybrid logic can be added to the logical framework LF, a constructive type theory of dependent functions. This extension turns out to be an attractively simple one, and maintains all the usual theoretical and algorithmic properties, for example decidability of type-checking. Moreover it results in a rich metalanguage for encoding and reasoning about a range of resource-sensitive substructural logics, analagous to the use of LF as a metalanguage for more ordinary logics.This family of applications of the language, contrary perhaps to expectations of how hybridized systems are typically used, does not require the usual modal connectives box and diamond, nor any internalization of a Kripke accessibility relation. It does, however, make essential use of distinctively hybrid connectives: universal quantifiation over worlds, truth of a proposition at a named world, and local binding of the current world. This supports the claim that the innovations of hybrid logic have independent value even apart from their traditional relationship to temporal and alethic modal logics.