Programming in dependent types
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.
- 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]
May 21, 2016 23:37 EET
local organizers, ewscs14(at)cs.ioc.ee
EWSCS'14 page: http://cs.ioc.ee/ewscs/2014/