This commit is contained in:
François Pottier 2017-10-12 15:47:05 +02:00
parent 8c50463ec4
commit 521f29c442

View file

@ -82,7 +82,15 @@ We also show the limits of dependently-typed functional programming.
closure conversion, defunctionalization closure conversion, defunctionalization
([slides 03](slides/fpottier-03.pdf)) ([slides 03](slides/fpottier-03.pdf))
([Coq repo](coq/)). ([Coq repo](coq/)).
* (13/10/2017) Compiling away the call stack: the CPS transformation. * (13/10/2017) Making the stack explicit: the CPS transformation
([slides 04](slides/fpottier-04.pdf))
([Coq repo](coq/)).
Transforming a call-by-value interpreter
([exercise](ocaml/EvalCBVExercise.ml), [solution](ocaml/EvalCBVCPS.ml)).
Transforming a call-by-name interpreter
([solution](ocaml/EvalCBNCPS.ml)).
Transforming a graph traversal
([solution](ocaml/Graph.ml)).
* (20/10/2017) Equational reasoning and program optimizations. * (20/10/2017) Equational reasoning and program optimizations.
### Metatheory of Typed Programming Languages ### Metatheory of Typed Programming Languages