Introduction to Dependently Typed Programming using Agda
Types guarantee properties of runtime behaviour. Dependent types give stronger guarantees based on runtime values. In this course we shall introduce dependently typed programming using the Agda programming language.
The course consists of five weekly afternoon sessions with lectures and hands-on laboratories. Exercises between sessions will be set. Refreshments will be provided during breaks.
Prerequisites: This is a research level course. We assume basic familiarity with a functional programming language, such as Haskell or ML, in particular pattern matching and higher-order functions like map.
This course is supported by the Scottish Informatics and Computer Science Alliance.
- Lab sessions will be held in lab 4.12, Appleton Tower.
- Lectures will take place in rooms G.03 or G.07A, Informatics Forum. See below.
Dates: Mondays, January 31, 2011 - February 28, 2011.Registration: Please let us know you are coming so we can prepare accordingly:
|Ohad Kammar <||ohad.kammar||@||ed.ac.uk>|
Course Material: All course material will be available online. Conor has set up a darcs repository that contains everything available currently. You can grab it from:
darcs get http://personal.cis.strath.ac.uk/~conor/pub/dtp
Mailing List: Course announcements, discussions and questions are welcome in the agda-course mailing list. Non registrants are welcome as well.
14:00–14:20: Coffee Break
15:20–15:40: Coffee Break
16:40–17:00: Coffee Break
31 January, 2011: First steps: Lists, Vectors and Peano Arithmetic
Location: IF G.03
07 February, 2011: Records, unit, sigma and finite sets.
Location: IF G.07A
14 February, 2011 Location: IF G.03
21 February, 2011 Location: IF G.03
28 February, 2011 Location: IF G.07A