Deciding and Interpolating Algebraic Data Types by Reduction (Technical Report)

Hossein Hojjat, Philipp Rümmer

Recursive algebraic data types (term algebras, ADTs) are one of the most well-studied theories in logic, and find application in contexts including functional programming, modellin…