Conor McBride - Dependently-Typed Metaprogramming 2/8: Metaprogramming the Simply-Typed λ-Calculus
Channel: Ohad Kammar
Date: 14/08/2013

Lecture 2 of 8 in Conor McBride's "Dependently-Typed Metaprogramming (in Agda)" given at the Cambridge University Computer Laboratory during August 2013.

Course materials (lecture notes, exercises) are available at the course webpage: http://www.cl.cam.ac.uk/~ok259/agda-course-13/