A blag containing my current adventures in logic, haskell and agents.

Sunday, 1 May 2011

Slides about Martin-Löf type theory

It's been a while since my last update. Anyway, last year, I participated in the seminar Dependently typed programming given by Andres Löh and Doaitse Swierstra. I gave a presentation, or more of a lecture really, about Martin-Löf type theory, the Curry-Howard correspondence and some of its connections with Agda.

Since I thought it would still be useful to share, here are the slides:
Type Systems

Download the slides here.