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).