[TYPES/announce] Course: Dependently typed metaprogramming (in Agda)

[Ohad Kammar]

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

****    Dependently typed metaprogramming (in Agda)   ****
by Conor McBride, MSP, University of Strathclyde

More information available at:
http://www.cl.cam.ac.uk/~ok259/agda-course-13/

Location
=======
Computer Laboratory, Cambridge, England

Description
=========

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/


Dates
=====

* Monday, 5 August, 2013.
* Wednesday, 7 August, 2013.
* Monday, 26 August, 2013.
* Wednesday 28 August, 2013.

Registration
==========

Please let us know you are coming so we can prepare accordingly,
please email your name and affilliation to

Ohad Kammar   <agda-course-2013-request @ cl.cam.ac.uk>


More information available at:
---------------------------------------
http://www.cl.cam.ac.uk/~ok259/agda-course-13/

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