Skip to Main content Skip to Navigation
Journal articles

An Open Logical Framework

Abstract : The LFP 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 Star-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 LFP, 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 LFP 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 LFP. We investigate and characterize the meta-theoretical properties of the calculus underpinning LFP : 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 LFP, based on a suitable extension of the notion of βη-long normal form, allowing for smooth formulations of adequacy statements.
Complete list of metadata

Cited literature [36 references]  Display  Hide  Download
Contributor : Luigi Liquori Connect in order to contact the contributor
Submitted on : Wednesday, November 20, 2013 - 12:38:19 PM
Last modification on : Wednesday, November 21, 2018 - 11:16:01 AM
Long-term archiving on: : Friday, February 21, 2014 - 4:24:01 AM


Files produced by the author(s)




Furio Honsell, Marina Lenisa, Luigi Liquori, Petar Maksimovic, Ivan Scagnetto. An Open Logical Framework. Journal of Logic and Computation, Oxford University Press (OUP), 2013, 25 (2), 43 p. ⟨10.1093/logcom/ext028⟩. ⟨hal-00906391⟩



Les métriques sont temporairement indisponibles