Haskell's Show Class in Isabelle/HOL

Christian Sternagel and René Thiemann

29 July 2014

Abstract

We implemented a type class for "to-string" functions, similar to Haskell's Show class. Moreover, we provide instantiations for Isabelle/HOL's standard types like bool, prod, sum, nats, ints, and rats. It is further possible, to automatically derive show functions for arbitrary user defined datatypes similar to Haskell's "deriving Show".
GNU Lesser General Public License (LGPL)

Change history

[2015-03-11] Adapted development to new-style (BNF-based) datatypes.
[2015-04-10] Moved development for old-style datatypes into subdirectory "Old_Datatype".

Depends On

Used by

Topics

Theories

Cite

×
@article{Show-AFP,
  author  = {Christian Sternagel and René Thiemann},
  title   = {Haskell's Show Class in Isabelle/HOL},
  journal = {Archive of Formal Proofs},
  month   = July,
  year    = 2014,
  note    = {\url{http://isa-afp.org/entries/Show.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
Download