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

Fix lists.

Browse source
This commit is contained in:
François Pottier 2017-09-11 10:41:47 +02:00
parent 0b50ea13f2
commit 7747bcfe3b
1 changed files with 20 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

40
README.md
View file

@ -52,34 +52,34 @@ We also show the limits of dependently-typed functional programming.
### Functional Programming: Under the Hood ### Functional Programming: Under the Hood
* (22/09/2017) From a small-step operational semantics... * (22/09/2017) From a small-step operational semantics...
* (29/09/2017) ... to an efficient interpreter. (2 weeks.) * (29/09/2017) ... to an efficient interpreter. (2 weeks.)
* (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.
### Metatheory of Typed Programming Languages ### Metatheory of Typed Programming Languages
First lesson on Sep 15, other lessons on Oct 27, Nov 02, 17, 24. First lesson on Sep 15, other lessons on Oct 27, Nov 02, 17, 24.
* Metatheory of System F. (Type soundness. Erasure.) * Metatheory of System F. (Type soundness. Erasure.)
* ADTs, existential types, GADTs. (Typed program transformations.) * ADTs, existential types, GADTs. (Typed program transformations.)
* Logical relations. * Logical relations.
* Subtyping. Rows. (Covariant arrays and covariant functions!) * Subtyping. Rows. (Covariant arrays and covariant functions!)
* References. (Value restriction.) * References. (Value restriction.)
### Advanced Aspects of Type Systems ### Advanced Aspects of Type Systems
* Exceptions and effect handlers. (Compiled away via CPS.) * Exceptions and effect handlers. (Compiled away via CPS.)
* Typechecking exceptions and handlers. * Typechecking exceptions and handlers.
* Type inference. (ML. Bidirectional. Elaboration.) * Type inference. (ML. Bidirectional. Elaboration.)
* Data/control flow analysis. * Data/control flow analysis.
* Functional correctness. Intro to dependent/refinement types. * Functional correctness. Intro to dependent/refinement types.
### Dependently-typed Functional Programming ### Dependently-typed Functional Programming
* Effectful functional programming. * Effectful functional programming.
* Dependent functional programming. * Dependent functional programming.
* Total functional programming. * Total functional programming.
* Generic functional programming. * Generic functional programming.
* Open problems in dependent functional programming. * Open problems in dependent functional programming.