GTReification
A working group on the topic of reification, generic tactics and type classes will take place on thursday march 31th at INRIA Paris (23 avenue d'Italie, 5th floor in the orange room), starting at 9.30am. The goal of this meeting is to review existing efforts to support reification and develop generic tactics and libraries using type classes in Coq and discuss further research directions in that area. The program is as follows:
- 9.30am: Coffee
- 10am: Reification and type classes for formalization in ATBR, AAC and ring by D. Pous (with the atbr.v demo file)
- 10.45am: Type Classes for Mathematics in Type Theory, by R. Krebbers
- 11.45am: Typeclasses and rings, non-commutative and commutative by Loïc Pottier
- 12.30pm: Lunch
- 2pm: Discussion
- Reification:
- Tool support
- Common infrastructure
- Efficiency concerns
- Generic tactics:
- Generalized use of typeclasses
- Repository of standard structures
- Type Classes: issues and wishes
- Reification:
- 4.30 Coffee break
If you would like a particular point to be discussed, please add it to the discussion item.
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.