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

• Published in: Canadian Journal of Zoology
• 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é Paris Cité (UPCité), Logical Time for Formal Embedded System Design (KAIROS), Centre Inria d'Université Côte d'Azur (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-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 (1965 - 2019) (UNS)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UniCA)-Université Nice Sophia Antipolis (1965 - 2019) (UNS)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UniCA)-Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), Université Nice Sophia Antipolis (1965 - 2019) (UNS)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UniCA)-Université Nice Sophia Antipolis (1965 - 2019) (UNS)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UniCA)
• Format: Conference Object
• Language: English
• Published: 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.science/hal-02573605; https://hal.science/hal-02573605v1/document; https://hal.science/hal-02573605v1/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...