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

Nested lists.

Browse source
This commit is contained in:
François Pottier 2017-10-13 09:28:58 +02:00
parent de8d6fedd9
commit 8d78692d88
1 changed files with 9 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
README.md
View file

@ -68,9 +68,9 @@ We also show the limits of dependently-typed functional programming.
Introduction ([slides 00](slides/fpottier-00.pdf)). Introduction ([slides 00](slides/fpottier-00.pdf)).
Syntax and operational semantics, on paper and on a machine Syntax and operational semantics, on paper and on a machine
([slides 01a](slides/fpottier-01a.pdf)) ([slides 01a](slides/fpottier-01a.pdf))
([slides 01b](slides/fpottier-01b.pdf)) ([slides 01b](slides/fpottier-01b.pdf)).
([OCaml solution to Newton-Raphson exercise](ocaml/NewtonRaphson.ml)) * Newton-Raphson in OCaml ([solution](ocaml/NewtonRaphson.ml)).
([Even.v](coq/Even.v)). * 1 is not even in Coq ([Even.v](coq/Even.v)).
* (29/09/2017) * (29/09/2017)
From a small-step semantics down to an efficient verified interpreter, From a small-step semantics down to an efficient verified interpreter,
in several stages in several stages
@ -85,12 +85,12 @@ We also show the limits of dependently-typed functional programming.
* (13/10/2017) Making the stack explicit: the CPS transformation * (13/10/2017) Making the stack explicit: the CPS transformation
([slides 04](slides/fpottier-04.pdf)) ([slides 04](slides/fpottier-04.pdf))
([Coq repo](coq/)). ([Coq repo](coq/)).
Transforming a call-by-value interpreter * Transforming a call-by-value interpreter
([exercise](ocaml/EvalCBVExercise.ml), [solution](ocaml/EvalCBVCPS.ml)). ([exercise](ocaml/EvalCBVExercise.ml), [solution](ocaml/EvalCBVCPS.ml)).
Transforming a call-by-name interpreter * Transforming a call-by-name interpreter
([solution](ocaml/EvalCBNCPS.ml)). ([solution](ocaml/EvalCBNCPS.ml)).
Transforming a graph traversal * Transforming a graph traversal
([solution](ocaml/Graph.ml)). ([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