A Type Checker for a Logical Framework with Union and Intersection Types (System Description)
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...
Main Authors: | , |
---|---|
Format: | Conference Object |
Language: | English |
Published: |
Schloss Dagstuhl - Leibniz-Zentrum für Informatik
2020
|
Subjects: | |
Online Access: | https://dx.doi.org/10.4230/lipics.fscd.2020.37 https://drops.dagstuhl.de/opus/volltexte/2020/12359/ |