Name
Abstract | ||
|---|---|---|
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.
|
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/978-3-642-03359-9_23 | Theorem Proving in Higher Order Logics |
Keywords | Field | DocType |
type inference,dependent record,classical setting,packaging mathematical structures,generic design pattern,broad variety,automated structure inference,algebraic structure,coq system,choice operator,discrete logarithm,matrix decomposition,multiple inheritance,design pattern | Mathematical structure,Inference,Algebraic structure,Computer science,Axiom,Matrix decomposition,Algorithm,Type inference,Theoretical computer science,Lemma (mathematics),Algebraically closed field | Conference |
Volume | ISSN | Citations |
5674 | 0302-9743 | 43 |
PageRank | References | Authors |
2.06 | 16 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| François Garillot | 1 | 160 | 7.53 |
| Georges Gonthier | 2 | 2275 | 195.06 |
| Assia Mahboubi | 3 | 308 | 20.84 |
| Laurence Rideau | 4 | 253 | 16.08 |