Workshop on reification and generic tactics

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
• 4.30 Coffee break

If you would like a particular point to be discussed, please add it to the discussion item.