LaxF: Side Conditions and External Evidence as Monads

We extend the constructive dependent type theory of the Logical Framework LF with a family of monads indexed by predicates over typed terms. These monads express the effect of factoring-out, postponing, or delegating to an external oracle the verification of a constraint or a side-condition. This new framework, called Lax Logical Framework, L ax F, is a conservative extension of LF, and hence it is the appropriate metalanguage for dealing formally with side-conditions or external evidence in logical systems. L ax F is the natural strengthening of LF p (the extension of LF introduced by the authors together with Marina Lenisa and Petar Maksimovic), which arises once the monadic nature of the lock constructors of LF p is fully exploited. The nature of these monads allows to utilize the unlock destructor instead of Moggi's monadic let T, thus simplifying the equational theory. The rules for the unlock allow us, furthermore, to remove the monadic constructor once the constraint is satisfied. By way of example we discuss the encodings in L ax F of call-by-value λ-calculus, Hoare's Logic, and Elementary Affine Logic.