Seminar and crash course on advanced type theory and formal logic (for vegetables).
This page is to be updated on the way.
Implementation language: Agda .
Striked out things are topics that weren’t covered explictly. You’re expected to do them yourself. A bit of philosophy and suffering. HOWTO: Get Started with Agda (i.e. how to install and configure Agda and Emacs) | 
Universes and Pure Type Systems (PTS)
 Wiki, “Agda Homepage.” [Online]. Available: http://wiki.portal.chalmers.se/agda/
 U. Norell, “Dependently Typed Programming in Agda.” [Online]. Available: http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf
 D. Peebles, “Introduction to Agda.” [Online]. Available: http://www.youtube.com/playlist?p=B7F836675DCE009C
 C. McBride, “Introduction to Dependently Typed Programming using Agda.” [Online]. Available: http://www.youtube.com/playlist?list=PL44F162A8B8CB7C87
 J. Malakhovski, “HOWTO: Get Started with Agda.” [Online]. Available: http://blog.oxij.org/2011/12/22/howto-get-started-with-agda/