hierarchy-builder
| swMATH ID: | 47022 |
| Software Authors: | Cohen, C.; Sakaguchi, K.; Tassi, E. |
| Description: | Hierarchy Builder (HB) provides high level commands to declare a hierarchy of algebraic structure (or interfaces if you prefer the glossary of computer science) for the Coq system. Given a structure one can develop its theory, and that theory becomes automatically applicable to all the examples of the structure. One can also declare alternative interfaces, for convenience or backward compatibility, and provide glue code linking these interfaces to the structures part of the hierarchy. HB commands compile down to Coq modules, sections, records, coercions, canonical structure instances and notations following the packed classes discipline which is at the core of the Mathematical Components library. All that complexity is hidden behind a few concepts and a few declarative Coq commands. |
| Homepage: | https://drops.dagstuhl.de/storage/00lipics/lipics-vol167-fscd2020/LIPIcs.FSCD.2020.34/LIPIcs.FSCD.2020.34.pdf |
| Source Code: |
 https://github.com/math-comp/hierarchy-builder
|
| Dependencies: | Coq |
| Related Software: | GitHub; Coq; mathlib; Mathematical Components; Lean; Agda; Isabelle/HOL; finmap; Coquelicot; Nuprl; PCM library; Matita; PVS; Metamath; Mizar; FreeSpec; OCaml; Monae; Andromeda; Isabelle |
| Cited in: | 6 Documents |
all
top 5
Cited by 11 Authors
| 4 | Affeldt, Reynald |
| 2 | Cohen, Cyril |
| 2 | Sakaguchi, Kazuhiko |
| 1 | Garrigue, Jacques |
| 1 | Kerjean, Marie |
| 1 | Mahboubi, Assia |
| 1 | Nowak, David E. |
| 1 | Rouhling, Damien |
| 1 | Saikawa, Takafumi |
| 1 | Saito, Ayumu |
| 1 | Wieser, Eric |
Cited in 2 Serials
| 1 | Journal of Automated Reasoning |
| 1 | Journal of Functional Programming |
Cited in 2 Fields
| 6 | Computer science (68-XX) |
| 1 | Mathematical logic and foundations (03-XX) |
