Generic functional programming is about defining generic functions by induction on the definition of a datatype. Basic examples of generic functions are generic equality tests and generic map functions. In this talk I will show how the techniques of generic programming can be naturally represented using dependent types. I will also show how to write generic proofs in this setting. I will extend Martin-Löf's logical framework for dependent types with a special universe of codes for inductive datatypes, and generic formation, introduction, elimination, and equality rules. The generic programs and proofs presented have been implemented in the proof assistant Agda/Alfa developed at Chalmers.

The talk is based on joint work with Marcin Benke and Patrik Jansson, Chalmers.