TTFV

Type Theory for Vegetables

Seminar and crash course on advanced type theory and formal logic (for vegetables).

This page is to be updated on the way.

Meetings

Contacts

Resources

Implementation language: Agda [1].

Language tutorials:

Plan

Striked out things are topics that weren’t covered explictly. You’re expected to do them yourself.

Checklist

References

[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/