diff --git a/README.md b/README.md
index 6a98ffc..04a0c3f 100644
--- a/README.md
+++ b/README.md
@@ -69,7 +69,14 @@ 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.)
+* [(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) 
+  of course notes.
+  
 * (27/10/2017) ADTs, existential types, GADTs. 
 * (03/11/2017) Logical relations.
 * (10/11/2017) Subtyping. Rows.