19th Estonian Winter School in Computer Science (EWSCS)
XIX Eesti Arvutiteaduse Talvekool

Palmse, Estonia, March 2 - 7, 2014

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

Valid CSS! Valid XHTML 1.0 Strict Last changed May 21, 2016 23:37 EET by local organizers, ewscs14(at)cs.ioc.ee
EWSCS'14 page: http://cs.ioc.ee/ewscs/2014/