Canonical Regular Types

Ethan K. Jackson, Nikolaj Bjørner & Wolfram Schulte
Regular types represent sets of structured data, and have been used in logic programming (LP) for verification. However, first-class regular type systems are uncommon in LP languages. In this paper we present a new approach to regular types, based on type canonization, aimed at providing a practical first-class regular type system.