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

• Main Authors: Liquori, Luigi, Stolze, Claude
• Format: Article in Journal/Newspaper
• Language: unknown
• Published: arXiv 2020
• Subjects: Logic in Computer Science cs.LO; Programming Languages cs.PL; FOS Computer and information sciences; F.3.1; F.4.1; Lambda; Beluga; Beluga*
• Online Access: https://dx.doi.org/10.48550/arxiv.2002.10803; https://arxiv.org/abs/2002.10803

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 intersection types, as described in previous papers by the authors. Bull also implements a subtyping algorithm for the Type...