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.

# Dependently typed type checking

Reply