A Type Checker for a Logical Framework with Union and Intersection Types

Luigi Liquori, Claude Stolze

We present the syntax, semantics, and typing rules of Bull, a prototype theorem prover based on the Delta-Framework, i.e. a fully-typed lambda-calculus decorated with union and int…