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.


  1. Great presentation. Do you happen to have a direct link to the pdf?

  2. Is there maybe a video of the presentation?

  3. You can use the Scribd DDL: http://www.scribd.com/document_downloads/54313539?extension=pdf

    There wasn't any video at the lecture sadly.

  4. Nebasuke, I was asking about an alternative location for the pdf, since I have neither a facebook or scribd account. No worries if that doesn't exist, just checking.

  5. Okay, sorry for your trouble then, I did not know you needed a scribd account for that. I've looked up how to access my new university space and uploaded it there: http://www.students.science.uu.nl/~3448584/TypeSystems.pdf

  6. Thanks a lot!