The LFP Framework is an extension of the Harper-Honsell-Plotkin's Edinburgh Logical Framework 
LF with predicates. This is accomplished by defining lock type constructors, which are a sort
of diamond-modality constructors, releasing their argument under the condition that a predicate, possibly
external to the system, 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 Poincare` 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 beta-eta-long normal form, allowing
for smooth formulations of adequacy statements.