Introduction to Dependently Typed Programming using Agda

Conor McBride

MSP, University of Strathclyde

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.

Location:

• 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.

Schedule:

13:00–14:00: Laboratory

14:00–14:20: Coffee Break

14:20–15:20: Lecture

15:20–15:40: Coffee Break

15:40–16:40: Lecture

16:40–17:00: Coffee Break

17:00–18:00: Laboratory

18:00-…: Pub…

Past Lectures:

1. 31 January, 2011: First steps: Lists, Vectors and Peano Arithmetic
   Location: IF G.03
   Exercises: 1.1–1.8.
   Video

2. 07 February, 2011: Records, unit, sigma and finite sets.
   Location: IF G.07A
   Exercises: 1.9–1.14.

Upcoming Lectures:

1. 14 February, 2011 Location: IF G.03

2. 21 February, 2011 Location: IF G.03

3. 28 February, 2011 Location: IF G.07A