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

Links from README.md to the slides and OCaml/Coq files.

Browse source
This commit is contained in:
François Pottier 2017-09-29 17:32:32 +02:00
parent fb3e42ac0d
commit a6d9506bd0
1 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
README.md
View file

@ -72,9 +72,12 @@ We also show the limits of dependently-typed functional programming.
([OCaml solution to Newton-Raphson exercise](ocaml/NewtonRaphson.ml)) ([OCaml solution to Newton-Raphson exercise](ocaml/NewtonRaphson.ml))
([Even.v](coq/Even.v)). ([Even.v](coq/Even.v)).
* (29/09/2017) * (29/09/2017)
From a small-step semantics down to an efficient interpreter, From a small-step semantics down to an efficient verified interpreter,
in several stages in several stages
([Coq demo](coq/DemoSyntaxReduction.v)). ([Coq demo](coq/DemoSyntaxReduction.v))
([slides 02](slides/fpottier-02.pdf))
([OCaml code](ocaml/Lambda.ml))
([Coq repo](coq/)).
* (06/10/2017) Compiling away first-class functions: closure conversion, defunctionalization. * (06/10/2017) Compiling away first-class functions: closure conversion, defunctionalization.
* (13/10/2017) Compiling away the call stack: the CPS transformation. * (13/10/2017) Compiling away the call stack: the CPS transformation.
* (20/10/2017) Equational reasoning and program optimizations. * (20/10/2017) Equational reasoning and program optimizations.