[TYPES/announce] Course: Introduction to Dependently Typed Programming using Agda

[Ohad Kammar]

LFCS, University of Edinburgh presents:

****      Introduction to Dependently Typed Programming using Agda  ****
by Conor McBride, MSP, University of Strathclyde

More information available at:
http://homepages.inf.ed.ac.uk/s0894694/agda-course/

Location
=======
School of Informatics, University of Edinburgh, Scotland.

Description
=========
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.

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      at     ed.ac.uk>

More information available at:
---------------------------------------
 http://homepages.inf.ed.ac.uk/s0894694/agda-course/

-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.