SourceForge.net Logo
project summary

 

Generating linear orders for datatypes

Title: Generating linear orders for datatypes
Author: René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at)
Submission date: 2012-08-07
Abstract: We provide a framework for registering automatic methods to derive class instances of datatypes, as it is possible using Haskell's ``deriving Ord, Show, ...'' feature.

We further implemented such automatic methods to derive (linear) orders or hash-functions which are required in the Isabelle Collection Framework. Moreover, for the tactic of Huffman and Krauss to show that a datatype is countable, we implemented a wrapper so that this tactic becomes accessible in our framework.

Our formalization was performed as part of the IsaFoR/CeTA project. With our new tactic we could completely remove tedious proofs for linear orders of two datatypes.

BibTeX:
@article{Datatype_Order_Generator-AFP,
  author  = {René Thiemann},
  title   = {Generating linear orders for datatypes},
  journal = {Archive of Formal Proofs},
  month   = aug,
  year    = 2012,
  note    = {\url{http://afp.sf.net/entries/Datatype_Order_Generator.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License