×

A coalgebraic foundation for coinductive union types. (English) Zbl 1409.68177

Esparza, Javier (ed.) et al., Automata, languages, and programming. 41st international colloquium, ICALP 2014, Copenhagen, Denmark, July 8–11, 2014. Proceedings, Part II. Berlin: Springer. Lect. Notes Comput. Sci. 8573, 62-73 (2014).
Summary: This paper introduces a coalgebraic foundation for coinductive types, interpreted as sets of values and extended with set theoretic union. We give a sound and complete characterization of semantic subtyping in terms of inclusion of maximal traces. Further, we provide a technique for reducing subtyping to inclusion between sets of finite traces, based on approximation. We obtain inclusion of tree languages as a sound and complete method to show semantic subtyping of recursive types with basic types, product and union, interpreted coinductively.
For the entire collection see [Zbl 1291.68018].

MSC:

68Q65 Abstract data types; algebraic specification
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Software:

XDuce; CDuce
PDFBibTeX XMLCite
Full Text: DOI