Conor McBride
Dept. of Computer and Information Sciences
University of Strathclyde
United Kingdom
Programming in dependent types
Abstract
These lectures will introduce concepts and techniques for giving more precise types to programs and data, ensuring that more desirable properties hold just by typechecking, in contrast to approaches which emphasize proof. The four lectures will cover (i) size and shape invariants, (ii) order and balance invariants, (iii) typesafe representations of embedded languages, and (iv) datatype generic programming. Most of the methods should be applicable in any functional language with dependent types, or a close enough approximation to them: it should be possible to do the exercises in Haskell or OCaml, as well as in Idris, Agda, or (perhaps with more effort) Coq.
Course materials
- C. McBride. Agda files for this course. link to github repo.
- Videos from the lectures.
- C. McBride. Dependently typed metaprogramming (in Agda). Notes, 2013. [pdf]
- C. McBride. How to keep your neighbours in order. Draft, 2014.
- C. McBride. Outrageous but meaningful coincidences: dependent type-safe syntax and evaluation. In Proc. of 2010 ACM SIGPLAN Wksh. on Generic Programming, WGP 2010, pp. 1-12. ACM Press, 2010. [doi link]
- J. Chapman, P.-É. Dagand, C. McBride, P. Morris. The gentle art of levitation. In Proc. of 15th ACM SIGPLAN Int. Conf. on Functional Programming, ICFP 2010, pp. 3-14. ACM Press, 2010. [doi link]
Last changed
May 21, 2016 23:37 EET
by
local organizers, ewscs14(at)cs.ioc.ee
EWSCS'14 page:
//cs.ioc.ee/ewscs/2014/