From 997801873bcc0cad6b71d5e1c404e3e6656f971b Mon Sep 17 00:00:00 2001 From: REMY Didier Date: Fri, 15 Sep 2017 08:52:43 +0200 Subject: [PATCH] slides and notes --- README.md | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index 04a0c3f..5985b1c 100644 --- a/README.md +++ b/README.md @@ -70,13 +70,11 @@ We also show the limits of dependently-typed functional programming. ### Metatheory of Typed Programming Languages * [(15/09/2017)] - [Metatheory of System F. (Type soundness. Erasure) - ](http://gallium.inria.fr/~remy/mpri/slides1.pdf) - [Intro](http://gallium.inria.fr/~remy/mpri/slides8.pdf) - See also [chap 1](http://gallium.inria.fr/~remy/mpri/2016/cours1.pdf) - and [chap 2](http://gallium.inria.fr/~remy/mpri/2016/cours2.pdf) + [Metatheory of System F](http://gallium.inria.fr/~remy/mpri/slides1.pdf) + See also [Intro](http://gallium.inria.fr/~remy/mpri/slides8.pdf), + and chap [1](http://gallium.inria.fr/~remy/mpri/2016/cours1.pdf) + and [2](http://gallium.inria.fr/~remy/mpri/2016/cours2.pdf) of course notes. - * (27/10/2017) ADTs, existential types, GADTs. * (03/11/2017) Logical relations. * (10/11/2017) Subtyping. Rows.