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