Introduction to Dependently Typed Programming (WiSe 2019)
| Dozent | Sergey Goncharov |
| Vorlesung/Übungen | Mo 16:15 – 17:45, 01.021; Di 16:15 – 17:45, 00.131-128 |
| Zielgruppe | WF M-BA ab 3 (ECTS-Credits: 7,5) WPF INF-BA-V-THI ab 4 (ECTS-Credits: 7,5) WPF INF-MA ab 1 (ECTS-Credits: 7,5) WF M-MA ab 1 (ECTS-Credits: 7,5) |
(Geeignet als WPF für Nebenfach Informatik in verschiedenen Studiengängen, insbesondere Mathematik.)
Übungsblätter
- Assignment 1 Code Template
- Assignment 2
- Assignment 3 Code Template for Exercise 2
- Assignment 4 Code Template for Exercise 1
- Assignment 5
Misc Agda Files
- “Example of mutual induction
- “Runnung summs
- “Equational reasoning (adapted from the standard libary)
- “De Morgan Laws and the Axiom of Choice
- “Example of based path induction
Quellenverzeichnis
- Philip Wadler, Wen Kokke, Jeremy Siek, Programming Language Foundations in Agda.
- Aaron Stump, Verified Functional Programming in Agda
- Agda 2.6 Documentation
- Recent version of The Iowa Agda Library (IAL): https://github.com/cedille/ial