We discuss the treatment of initial datatypes and final process types in the wide-spectrum language HASCASL. In particular, we present specifications that illustrate how datatypes and process types arise as bootstrapped concepts using HASCASL'S type class mechanism, and we decribe constructions of types of finite and infinite trees that establish the conservativity of datatype and process type declarations adhering to certain reasonable formats. The latter amounts to modifying known constructions from HOL to avoid unique choice; in categorical terminology, this means that we establish that quasitoposes with an internal natural numbers object support initial algebras and final coal-gebras for a range of polynomial functors, thereby partially generalizing corresponding results from topos theory. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Schröder, L. (2007). Bootstrapping types and cotypes in HASCASL. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4624 LNCS, pp. 447–461). Springer Verlag. https://doi.org/10.1007/978-3-540-73859-6_30
Mendeley helps you to discover research relevant for your work.