Slides for “An Algebraic Approach to Typechecking and Elaboration”
Two months at the Scottish Programming Languages Seminar, February 2015 Strathclyde Edition, I gave a talk entitled “An Algebraic Approach to Typechecking and Elaboration”. Several people have asked me to put the slides online, so here they are:
The point of the talk was to present an algebraic approach to specifying type systems ─ algebraic in the sense of algebraic theories with operations and equations. I reckon this presentation leads naturally to a unification of the way that typed functional languages like ML and Haskell elaborate their source language into explicitly typed core languages, and the tactic languages in interactive theorem provers like Coq and Isabelle.
Update: (2015-05-20) I gave this talk again at the Workshop on Type Inference and Automated Proving in Dundee, and it was recorded (link to video).
Update: (2015-09-03) I gave this talk a third time at the Higher Order Programming with Effects (HOPE) workshop colocated with ICFP 2015 in Vancouver, and it was again recorded (link to video).