Name
Abstract | ||
|---|---|---|
Proof assistants such as the Coq system have traditionally been a laboratory for exotic type features such as dependent and computable types, and first-class type classes. Although these features have been introduced independently, it turns out they can be com-bined in novel and nontrivial ways to solve some of the more challenging problems posed by the formalization of advanced mathematics. Many of these patterns could also be useful for general programming. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1145/1929553.1929555 | TLDI |
Keywords | Field | DocType |
reflection,type design pattern,general programming,computer mathematics,computable type,user notation,design patterns,nontrivial way,first-class type class,coq system,theorem proving,type inference,advanced mathematics,exotic type,type classes,challenging problem,proof assistant,generic programming,design pattern | Type design,Programming language,Computer science,Automated theorem proving,Software design pattern,Theoretical computer science,Type inference,Data type | Conference |
Citations | PageRank | References |
0 | 0.34 | 0 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Georges Gonthier | 1 | 2275 | 195.06 |