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

Conference paper

Schropp, A. and Popescu, A. 2013. Nonfree datatypes in Isabelle/HOL: animating a many-sorted metatheory. Certified Programs and Proofs (CPP). Melbourne, Australia 11 - 13 Dec 2013 Springer. pp. 114-130 https://doi.org/10.1007/978-3-319-03545-1_8
TypeConference paper
TitleNonfree datatypes in Isabelle/HOL: animating a many-sorted metatheory
AuthorsSchropp, A. and Popescu, A.
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.

Research GroupFoundations of Computing group
ConferenceCertified Programs and Proofs (CPP)
Page range114-130
ISSN0302-9743
ISBN
Hardcover9783319035444
PublisherSpringer
Publication dates
Print13 Dec 2013
Publication process dates
Deposited27 Apr 2015
Output statusPublished
Copyright Statement

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-03545-1_8

Additional information

Volume 8307 of the series Lecture Notes in Computer Science

Digital Object Identifier (DOI)https://doi.org/10.1007/978-3-319-03545-1_8
LanguageEnglish
Book titleCertified Programs and Proofs: third international conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceeding
File
Permalink -

https://repository.mdx.ac.uk/item/851zz

Log in to edit

Download files

  • 21
    total views
  • 13
    total downloads
  • 1
    views this month
  • 0
    downloads this month

Export as