Design and implementation in OCaml of a type checker for the LLFP Logical Framework

Vincent Michielini

ENS Lyon (France)

LFP (LF with Predicates) [4] is an extension of Harper-Honsell-Plotkin’s Edinburgh Logical Framework LF with locking type constructors. The latter are a sort of modality constructors, releasing their argument under the condition that a predicate, possibly external to the system, is satisfied on an appropriate typed judgement. This mechanism paves the way for a proof assistant allowing the user to make calls to external oracles (e.g., other proof assistants) during the proof development activity. Such calls are usually made to factor out the complexity of encoding specific features of logical systems which would otherwise be awkwardly encoded in LF, e.g. side-conditions in the application of rules in Modal Logics, and sub-structural rules, as in non- commutative Linear Logic. Using LFP, these conditions need only to be specified, while their verification can be delegated to an external proof engine, according to the Poincaré Principle. LLFP (Lax LFP) [5] is a further extension of Edinburgh LF with a family of monads indexed by predicates over typed terms. Beside factoring-out and delegating to an external oracle the verification of a constraint or a side-condition (as in LFP), these monads also express the effect of postponing such verifications. This fact allows the user to focus on the main proof, leaving the possibly external verification of details at the end. In this talk we will present a first prototype of a type checker written in OCaml (https://ocaml.org/) for the typing system of CLLFP [5], namely, the canonical version of LLFP, according to the implementation driven format of the CMU School [2]. We will conclude providing examples of external predicates related to the encodings of Modal Logics and of the Fitch-Prawitz Set Theory [1,6] in CLLFP.