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 [1].
Language tutorials:
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) | [5]
Universes and Pure Type Systems (PTS)
[1] Wiki, “Agda Homepage.” [Online]. Available: http://wiki.portal.chalmers.se/agda/
[2] U. Norell, “Dependently Typed Programming in Agda.” [Online]. Available: http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf
[3] D. Peebles, “Introduction to Agda.” [Online]. Available: http://www.youtube.com/playlist?p=B7F836675DCE009C
[4] C. McBride, “Introduction to Dependently Typed Programming using Agda.” [Online]. Available: http://www.youtube.com/playlist?list=PL44F162A8B8CB7C87
[5] J. Malakhovski, “HOWTO: Get Started with Agda.” [Online]. Available: http://blog.oxij.org/2011/12/22/howto-get-started-with-agda/