Commit da9cb531 authored by POTTIER Francois's avatar POTTIER Francois

Exchange of dates between Pottier and Rémy.

parent 9bd9820f
......@@ -104,20 +104,20 @@ We also show the limits of dependently-typed functional programming.
* Transforming a graph traversal
* (??/10/2019) Equational reasoning and program optimizations
* (18/10/2019, *to be confirmed*) Equational reasoning and program optimizations
([slides 05](slides/fpottier-05.pdf))
([Coq mini-demo](coq/DemoEqReasoning.v)).
### Metatheory of Typed Programming Languages
* (18/10/2019)
* (11/10/2019)
[Metatheory of System F](
(see also [intro](,
and chap [1,2,3](
and [4](
of [course notes](
* (25/10/2019)
* (25/10/2019, *to be confirmed*)
[ADTs, existential types, GADTs](
[without]( or
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment