The Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness for Algebraic Union, Intersection, Negation, and Equi-recursive Types (Artifact)
Abstract
Our paper presents a semantic proof for the soundness of Boolean-algebraic subtyping in MLstruct. Based on the completeness of characteristic homomorphisms, we propose an algorithm for deciding subtyping in the presence of union, intersection, negation, and equi-recursive types. This artifact implements the subtyping algorithm.
Publication details
- Journal / source
- Rare & Special e-Zone (The Hong Kong University of Science and Technology)
- Publication date
- 9 January 2026
- Language
- EN