Ohad's Research - Agda Course 2013

The Logic, Semantics, and Programming Languages Group at the University of Cambridge presents:

# Dependently typed metaprogramming (in Agda)

## 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 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

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:

git pull origin

#### 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:

1. 05 August, 2013: Introduction via Vectors
Location: SW01
Video

2. 05 August, 2013: Metaprogramming the Simply-Typed λ-Calculus
Location: SW01
Video

3. 07 August, 2013: Containers and W-Types
Location: SW01
Video

4. 07 August, 2013: Indexed Containers
Location: SW01
Video

5. 26 August, 2013: Induction-Recursion I
Location: SW01
Video

6. 26 August, 2013: Induction-Recursion II
Location: SW01
Video

7. 28 August, 2013: Observational Equality
Location: SW01
Video

8. 28 August, 2013: Type Theory in Type Theory
Location: SW01
Video

#### Acknowledgements

Thanks to Alan Mycroft for arranging the funding! And, of course, to Conor for preparing the course!