The LFP Framework is an extension of the Harper-Honsell-
Plotkin’s Edinburgh Logical Framework LF with external predicates.
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 LFP, one can
factor out the complexity of encoding specific features of logical
systems which, otherwise, would be awkwardly encoded in LF,
e.g. side-conditions in the application of rules in Modal Logics,
and substructural 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´e Principle.We investigate and characterize
the metatheoretical properties of the calculus underpinning LFP:
strong normalization, confluence, and subject reduction. This latter
property holds under the assumption that the predicates are wellbehaved,
i.e. closed under weakening, permutation, substitution,
and reduction in the arguments.
Keywords: Type theory, logical frameworks.