slides and notes
This commit is contained in:
parent
d235435edb
commit
1bd9634a2a
1 changed files with 8 additions and 1 deletions
|
@ -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.
|
||||
|
|
Loading…
Reference in a new issue