General information
The webpage of this course is here. I teach the third part which is entitled "Towards proved programs". We will discuss the different ways to extend static checking in order to go beyond safety. Feel free to send me an email if you are stuck on some aspect of these lectures. You can also contact me at yann.regisgianas on gmail's XMPP.
Lectures notes can be downloaded as a PDF file. (They only cover type checking of GADTs for now.) You can easily be up-to-date with respect to all the course material thanks to the git repository at:
git clone http://www.pps.jussieu.fr/~yrg/git/mpri-tpp
(By the way, patchs are welcomed!)
Introduction
You can download the slides.
Part I : Introducing Generalized Algebraic Datatypes
You can download the slides and look at the code samples (or here in a single HTML page).
The code samples require the current
development version of ocaml. You can compile it from the
subversion server.
Part II : Type Inference in ML extended with GADTs
You can download the slides.
Part III : Dependently typed programming
You can download the slides.
Part IV : Higher Order Hoare Logic
You can download the slides.