Thursday 10 October 2019, 14:00, LSV library: Type classes in Isabelle, Michael Färber (post-doc, deducteam, LSV).

Type classes were introduced by Wadler & Blott in 1988 as a disciplined approach to handle ad-hoc polymorphism via overloading of constants. Since then, type classes were integrated into several programming languages and proof assistants, such as Haskell and Isabelle. I will give an introduction to type classes in Isabelle and discuss how they could be translated to Dedukti.