I was purging the disk on my laptop of large files and found a video lecture which I forgot to publish. Here it is with some delay. I lectured on how to implement type theory at the School and Workshop on Univalent Mathematics in December 2017, at the University of Birmingham (UK).
I have had the honor to lecture at the Oregon Programming Language Summer School 2018 on the topic of algebraic effects and handlers. The notes, materials and the lectures are available online:
- the GitHub repository with the course material
- the OPLSS lecture materials, including notes and video recordings of the lectures
I gave four lectures which started with the mathematics of algebraic theories, explained how they can be used to model computational effects, how we make a programming language out of them, and how to program with handlers.
Mike Shulman just wrote a very nice blog post on what is a formal proof. I much agree with what he says, but I would like to offer my own perspective. I started writing it as a comment to Mike’s post and then realized that it is too long, and that I would like to have it recorded independently as well. Please read Mike’s blog post first.
I am about to give an invited talk at the Workshop on Categorical Logic and Univalent Foundations 2016 in Leeds, UK. It’s a charming workshop that I am enjoing a great deal. Here are the slides of my talk, with speaker notes, as well as the Andromeda examples that I am planning to cover.