This paper proposes generic design patterns to define and combine algebraic structures, using dependent records, coercions and type inference, inside the Coq system. This alternative to telescopes in particular supports multiple inheritance, maximal sharing of notations and theories, and automated structure inference. Our methodology is robust enough to handle a hierarchy comprising a broad variety of algebraic structures, from types with a choice operator to algebraically closed fields. Interfaces for the structures enjoy the convenience of a classical setting, without requiring any axiom. Finally, we present two applications of our proof techniques: a key lemma for characterising the discrete logarithm, and a matrix decomposition problem. © 2009 Springer.
CITATION STYLE
Garillot, F., Gonthier, G., Mahboubi, A., & Rideau, L. (2009). Packaging mathematical structures. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5674 LNCS, pp. 327–342). https://doi.org/10.1007/978-3-642-03359-9_23
Mendeley helps you to discover research relevant for your work.