Nonfree datatypes in Isabelle/HOL animating a many-sorted metatheory

7Citations
Citations of this article
4Readers
Mendeley users who have this article in their library.
Get full text

Abstract

Datatypes freely generated by their constructors are well supported in mainstream proof assistants. Algebraic specification languages offer more expressive datatypes on axiomatic means: nonfree datatypes generated from constructors modulo equations. We have implemented an Isabelle/HOL package for nonfree datatypes, without compromising foundations. The use of the package, and its nonfree iterator in particular, is illustrated with examples: bags, polynomials and λ-terms modulo α-equivalence. The many-sorted metatheory of nonfree datatypes is formalized as an ordinary Isabelle theory and is animated by the package into user-specified instances. HOL lacks a type of types, so we employ an ad hoc construction of a universe embedding the relevant parameter types. © Springer International Publishing 2013.

Cite

CITATION STYLE

APA

Schropp, A., & Popescu, A. (2013). Nonfree datatypes in Isabelle/HOL animating a many-sorted metatheory. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8307 LNCS, pp. 114–130). https://doi.org/10.1007/978-3-319-03545-1_8

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free