Skip to content
This repository has been archived by the owner on Jul 9, 2019. It is now read-only.

mietek/agda-intro

Repository files navigation


This is an archival copy of the original page. Please see the lecture videos.


LFCS, University of Edinburgh presents:

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 <…@…>

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:

  • 14 February, 2011 Location: IF G.03
  • 21 February, 2011 Location: IF G.03
  • 28 February, 2011 Location: IF G.07A

About

Mirror of Conor McBride’s 2011 Agda course materials

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages