Name
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 comparators, linear orders, parametrizable equality functions, and hashfunctions which are required in the Isabelle Collection Framework [1] and the Container Framework [2]. Moreover, for the tactic of Blanchette to show that a datatype is countable, we implemented a wrapper so that this tactic becomes accessible in our framework. All of the generators are based on the infrastructure that is provided by the BNF-based datatype package. Our formalization was performed as part of the IsaFoR/CeTA project [3]. With our new tactics we could remove several tedious proofs for (conditional) linear orders, and conditional equality operators within IsaFoR and the Container Framework. |
Year | Venue | Field |
|---|---|---|
2015 | Archive of Formal Proofs | Programming language,Countable set,Computer science,Mathematical proof,Haskell,Operator (computer programming) |
DocType | Volume | Citations |
Journal | 2015 | 1 |
PageRank | References | Authors |
0.35 | 3 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Christian Sternagel | 1 | 202 | 27.60 |
| René Thiemann | 2 | 984 | 69.38 |