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

• Main Authors: Stolze, Claude, Liquori, Luigi
• Other Authors: Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Centre National de la Recherche Scientifique (CNRS)-Université de Paris (UP), Logical Time for Formal Embedded System Design (KAIROS), COMmunications, Réseaux, systèmes Embarqués et Distribués (Laboratoire I3S - COMRED), Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), Université Nice Sophia Antipolis (. - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Université Nice Sophia Antipolis (. - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)
• Format: Conference Object
• Language: English
• Published: HAL CCSD 2020
• Subjects: 2012 ACM Subject Classification Theory of computation → Lambda calculus; Theory of computation → Proof theory Keywords and phrases Intersection types; Union types; Dependent types; Subtyping; Type checker; Refiner; ∆-Framework; [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL]; [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]; Lambda; Beluga; Beluga*
• Online Access: https://hal.archives-ouvertes.fr/hal-02573605; https://hal.archives-ouvertes.fr/hal-02573605/document; https://hal.archives-ouvertes.fr/hal-02573605/file/article.pdf; https://doi.org/10.4230/LIPIcs.FSCD.2020

International audience 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 pap...