Seminar and crash course on advanced type theory and formal logic (for vegetables).
@oxij
(in English) and/or @neoxij
(not only in English).Implementation language: Agda [1].
Language tutorials:
Striked out things are topics that weren’t covered explictly. You’re expected to do them yourself.
1. Agda Project Authors. Agda homepage. http://wiki.portal.chalmers.se/agda/.
2. Setzer A. Interactive theorem proving for agda users. http://www.cs.swan.ac.uk/~csetzer/lectures/intertheo/07/interactiveTheoremProvingForAgdaUsers.html.
3. Norell U. Dependently typed programming in agda. 2008. http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf.
4. Peebles D. Introduction to agda. http://www.youtube.com/playlist?p=B7F836675DCE009C.
5. McBride C. Introduction to dependently typed programming using agda. http://www.youtube.com/playlist?list=PL44F162A8B8CB7C87.
6. Malakhovski J. Введение в agda. http://www.youtube.com/watch?v=uUb-zItrYjQ.
7. Agda Wiki Authors. Agda tutorials list. 2015. http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Othertutorials.
8. Malakhovski J. HOWTO: Get started with agda. http://blog.oxij.org/2011/12/22/howto-get-started-with-agda/.