type design patterns for computer mathematics
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.
design patterns type classes reflection theorem proving user notation type inference