Sciweavers

ENTCS
2007

Hybridizing a Logical Framework

13 years 3 months ago
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 innov...
Jason Reed
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2007
Where ENTCS
Authors Jason Reed
Comments (0)