Title: $\mathsf{LLF}_{\cal P}$: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads,
Abstract: We extend the constructive dependent type theory of the Logical Framework
$\mathsf{LF}$ with monadic, dependent type constructors indexed with predicates
over judgements, called Locks. These monads capture various possible proof
attitudes in establishing the judgment of the object logic encoded by an
$\mathsf{LF}$ type. Standard examples are factoring-out the verification of a
constraint or delegating it to an external oracle, or supplying some
non-apodictic epistemic evidence, or simply discarding the proof witness of a
precondition deeming it irrelevant. This new framework, called Lax Logical
Framework, $\mathsf{LLF}_{\cal P}$, is a conservative extension of
$\mathsf{LF}$, and hence it is the appropriate metalanguage for dealing
formally with side-conditions in rules or external evidence in logical systems.
$\mathsf{LLF}_{\cal P}$ arises once the monadic nature of the lock
type-constructor, ${\cal L}^{\cal P}_{M,\sigma}[\cdot]$, introduced by the
authors in a series of papers, together with Marina Lenisa, is fully exploited.
The nature of the lock monads permits to utilize the very Lock destructor,
${\cal U}^{\cal P}_{M,\sigma}[\cdot]$, in place of Moggi's monadic $let_T$,
thus simplifying the equational theory. The rules for ${\cal U}^{\cal
P}_{M,\sigma}[\cdot]$ permit also the removal of the monad once the constraint
is satisfied. We derive the meta-theory of $\mathsf{LLF}_{\cal P}$ by a novel
indirect method based on the encoding of $\mathsf{LLF}_{\cal P}$ in
$\mathsf{LF}$. We discuss encodings in $\mathsf{LLF}_{\cal P}$ of call-by-value
$\lambda$-calculi, Hoare's Logic, and Fitch-Prawitz Naive Set Theory.