tobast/mpri-funcprog-project
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

English. (Plus spurious whitespace.)

Browse source
This commit is contained in:
François Pottier 2017-09-20 15:48:34 +02:00
parent 20967ac671
commit ace98b8d7a
1 changed files with 25 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
README.md
View file

@ -1,13 +1,15 @@
# Functional programming and type systems (2017-2018) # Functional programming and type systems (2017-2018)
[The official MPRI This page supplements
page](https://wikimpri.dptinfo.ens-cachan.fr/doku.php?id=cours:c-2-4-2) [the official page of MPRI 2-4](https://wikimpri.dptinfo.ens-cachan.fr/doku.php?id=cours:c-2-4-2).
## Location ## Location and duration
The lessons take place at University of Paris 7 - Denis Diderot, The lectures take place at University Paris 7 - Denis Diderot,
Batiment Sophie Germain in room 2035 on Fridays at 12:45 and ends at 15:30. Bâtiment Sophie Germain, in room 2035.
There will be a break of 15' in the middle of the course.
They are scheduled on Fridays from 12:45 to 15:30.
There is a 15-minute break in the middle of each lecture.
## Teachers ## Teachers
@ -43,8 +45,8 @@ systems. We study parametric polymorphism (as in System F and ML), data
types and type abstraction. We show syntactic type soundness (via progress types and type abstraction. We show syntactic type soundness (via progress
and subject reduction) by reasoning by induction on typing derivations. We and subject reduction) by reasoning by induction on typing derivations. We
also show how to obtain semantic properties via logical relations by also show how to obtain semantic properties via logical relations by
reasoning by induction on the structure of types. We also introduce reasoning by induction on the structure of types. Finally, we introduce
subtyping and row polymorphism and illustrate typing problems induced by subtyping, row polymorphism, and illustrate the problems induced by
side effects (references) and the need for the value restriction. side effects (references) and the need for the value restriction.
The third part of the course describes more advanced features of type The third part of the course describes more advanced features of type