A Type Checker for a Logical Framework with Union and Intersection Types
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...
Main Authors: | , |
---|---|
Format: | Article in Journal/Newspaper |
Language: | unknown |
Published: |
arXiv
2020
|
Subjects: | |
Online Access: | https://dx.doi.org/10.48550/arxiv.2002.10803 https://arxiv.org/abs/2002.10803 |