Personal tools
You are here: Home Events Course on Dependently typed metaprogramming (in Agda) by Conor McBride

Course on Dependently typed metaprogramming (in Agda) by Conor McBride

— filed under:

  • Upcoming events
When Nov 14, 2013 12:00 AM to
Dec 19, 2013 12:00 AM
Where 4.12, Appleton Tower and 2.33, Informatics Forum
Contact Name
Add event to calendar vCal

Dependently typed metaprogramming (in Agda)

by Conor McBride (MSP, 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 dependently-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.

This course receives financial support from the Complex Systems Engineering theme of SICSA, the Scottish Informatics and Computer Science Alliance.


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 earlier introductory Agda course held in Edinburgh can be found at:


  • Lectures (8 x 1 hour):
    • Informatics Forum, room 2.33, 3.30pm - 4.30pm and 5pm - 6pm.
    1.   Thursday, 14 November, 2013.
    2.   Thursday, 28 November, 2013.
    3.   Thursday, 12 December, 2013.
    4.   TBA
  • Lab sessions:
    •  Appleton tower, room 4.12, 2pm - 3pm
    • Thursday afternoons, starting on 14 November


Please let us know you are coming so we can prepare accordingly, please email your name and affilliation to the organizers:
  • Danel Ahman <D.Ahman {ät}>    
  • Sam Lindley <Sam.Lindley {ät}>

More details can be found on the course website.

Document Actions