|
LFCS, University of Edinburgh presents: Introduction to Dependently Typed Programming using AgdaConor McBrideMSP, 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:
Dates: Mondays, January 31, 2011 - February 28, 2011. Registration: Please let us know you are coming so we can prepare accordingly:
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: 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:
Upcoming Lectures:
|
