An open logical framework
Furio Honsell, Marina Lenisa, Ivan Scagnetto, Luigi Liquori, Petar Maksimović · Journal of Logic and Computation · 2013
The LF P Framework is an extension of the Harper–Honsell–Plotkin's Edinburgh Logical Framework LF with external predicates , hence the name Open Logical Framework . This is accomplished by defining lock type constructors , which are a sort of ⋄ -modality constructors , releasing their argument under the condition that a possibly external predicate is satisfied on an appropriate typed judgement. Lock types are defined using the standard pattern of constructive type theory, i . e . via introduction , elimination and equality rules . Using LF P , one can factor out the complexity of encoding specific features of logical systems, which would otherwise be awkwardly encoded in LF, e . g . side-conditions in the application of rules in Modal Logics, and sub-structural rules, as in non-commutative Linear Logic . The idea of LF P is that these conditions need only to be specified, while their verification can be delegated to an external proof engine, in the style of the Poincaré Principle or Deduction Modulo . Indeed such paradigms can be adequately formalized in LF P . We investigate and characterize the meta-theoretical properties of the calculus underpinning LF P : strong normalization, confluence and subject reduction. This latter property holds under the assumption that the predicates are well-behaved , i . e . closed under weakening, permutation , substitution and reduction in the arguments. Moreover, we provide a canonical presentation of LF P , based on a suitable extension of the notion of βη - long normal form , allowing for smooth formulations of adequacy statements.