The Logic, Semantics, and Programming Languages Group at the University of Cambridge presents: Dependently typed metaprogramming (in Agda)Conor McBrideMSP, University of Strathclyde Dependently typed functional programming languages such as Agda are capable of expressing very precise types for data. When those data themselves encode types, we gain a powerful mechanism for abstracting generic operations over carefully circumscribed universes. This course will begin with a rapid depedently-typed programming primer in Agda, then explore techniques for and consequences of universe constructions. Of central importance are the “pattern functors” which determine the node structure of inductive and coinductive datatypes. We shall consider syntactic presentations of these functors (allowing operations as useful as symbolic differentiation), and relate them to the more uniform abstract notion of “container”. We shall expose the double-life containers lead as “interaction structures” describing systems of effects. Later, we step up to functors over universes, acquiring the power of inductive-recursive definitions, and we use that power to build universes of dependent types. Prerequisites: This class assumes familiarity with typed functional programming, but will not require prior experience with depedently-typed programming nor with Agda. We do, however, recommend dabbling with Agda in advance. Materials from an introductory Agda course can be found at http://www.cl.cam.ac.uk/~ok259/agda-course and https://personal.cis.strath.ac.uk/conor.mcbride/pub/dtp/ Location:This course was given at the University of Cambridge Computer Laboratory Course Material:All course material will be available online.
After cloning the initial repository, don’t forget to pull the latest changes:
Mailing List:Course announcements, discussions and questions are welcome in the agda-course-2013 mailing list. Non-registrants: you are welcome to join too, please email Ohad in the address above to join, with some indication you are not a machine. 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:
AcknowledgementsThanks to Alan Mycroft for arranging the funding! And, of course, to Conor for preparing the course!
|