In this paper, we introduce a \emph{General Logical Framework},
  called \GLF, for defining Logical Frameworks, based on dependent
  types, in the style of the well known Edinburgh Logical Framework
  \LF.  The framework \GLF\ features a generalized form of lambda
  abstraction where $\beta$-reductions fire provided the argument
  satisfies a logical predicate and may produce an $n$-ary
  substitution. The type system \emph{keeps} track of when reductions
  have yet to fire.  The framework \GLF\ subsumes, by simple
  instantiation, \LF\ as well as a large class of generalized
  constrained-based lambda calculi, ranging from well known restricted
  lambda calculi, such as Plotkin's call-by-value lambda calculus, to
  lambda calculi with patterns. But it suggests also a wide spectrum
  of new calculi which have intriguing potential as Logical
  Frameworks.

  We investigate the metatheoretical properties of the calculus
  underpinning \GLF\ and illustrate its expressive power.  In
  particular, we focus on two interesting instantiations of \GLF. The
  first is the Pattern Logical Framework (\PLF), where applications
  fire via \emph{pattern-matching} in the style of Cirstea, Kirchner,
  and Liquori.  The second is the Closed Logical Framework (\CLF)
  which features, besides standard $\beta$-reduction, also a reduction
  which fires only if the argument is a \emph{closed} term.  For both
  these instantiations of \GLF\ we discuss standard metaproperties,
  such as subject reduction, confluence and strong normalization.

  The \GLF\ framework is particularly suitable, as a metalanguage, for
  encoding rewriting logics and logical systems, where rules require
  proof terms to have special syntactic constraints, \eg\ logics with
  \emph{rules of proof}, in addition to \emph{rules of derivations},
  such as, \eg, modal logic, and call-by-value lambda calculus.