The Logical-Logical Framework LLF is an extension of the Harper-Honsell-Plotkin’s Edinburgh Logical Framework LF with logical predicates. This is done by defining lock type constructors, which are a sort of ⋄ modality constructors, releasing their argument under the con- dition 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 and elimination rules. Using LLF, one can factor out the complexity of encoding specific fea- tures of logical systems which are awkward in LF, e.g. side-conditions in the application of rules in Modal Logics, or pre- and post-conditions in programming languages and logics. Once these conditions have been factored out, their verification can be delegated to an external proof en- gine, in the style of Poincar ́e Principle. We investigate and characterize the metatheoretical properties of the calculus underpinning LLF, such as strong normalization, confluence, subject reduction, and decidability.
