A Type Checker for a Logical Framework with Union and Intersection Types (System Description)

• Main Authors: Stolze, Claude, Liquori, Luigi
• Format: Conference Object
• Language: English
• Published: Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2020
• Subjects: Intersection types; Union types; Dependent types; Subtyping; Type checker; Refiner; Δ-Framework; Theory of computation → Lambda calculus; Theory of computation → Proof theory; Lambda; Beluga; Beluga*
• Online Access: https://dx.doi.org/10.4230/lipics.fscd.2020.37; https://drops.dagstuhl.de/opus/volltexte/2020/12359/

We present the syntax, semantics, typing, subtyping, unification, refinement, and REPL of BULL, a prototype theorem prover based on the Δ-Framework, i.e. a fully-typed Logical Framework à la Edinburgh LF decorated with union and intersection types, as described in previous papers by the authors. BUL...