Dependently typed type checking

Today we discussed a type checker for simply typed lambda calculus written in Agda that Ulf Norell presented in his ICFP 2013 invited talk. Another version can be found in The view from the left by Conor McBride and James McKinna.

Advertisements

Homotopy before type theory

Last Friday, the 18th of October, I talked about homotopy and the fundamental group. As I heard about homotopy type theory, I thought that reviewing what I know of the geometric part could be useful. So I prepared this talk, using Allen Hatcher’s free textbook.

Consider a continuous line on the whiteboard, from point x_0 to point x_1, and another continuous line from point y_0 to point y_1. Think of a bijection between the two lines: Continue reading