Plugging-in proof development environments using Locks in LF

We present two extensions of the LF constructive type theory featuring monadic locks. A lock is a monadic type construct that captures the effect of an external call to an oracle. Such calls are the basic tool for plugging-in and gluing together, different metalanguages and proof development environments. Oracles can be invoked either to check that a constraint holds or to provide a witness. The systems are presented in the canonical style developed by the ‘CMU School.’ The first system, CLLF, is the canonical version of the system LLF, presented earlier by the authors. The second system, CLLF?, features the possibility of invoking the oracle to obtain also a witness satisfying a given constraint. In order to illustrate the advantages of our new frameworks, we show how to encode logical systems featuring rules that deeply constrain the shape of proofs. The locks mechanisms of CLLF and CLLF? permit to factor out naturally the complexities arising from enforcing these ‘side conditions,’ which severely obscure standard LF encodings. We discuss Girard's Elementary Affine Logic, Fitch–Prawitz set theory, call-by-value λ-calculi and functions, both total and even partial.