mpri-funcprog-project/README.md

101 lines
4.4 KiB
Markdown
Raw Normal View History

2017-09-11 10:40:02 +02:00
# Functional programming and type systems (2017-2018)
2017-09-11 10:29:22 +02:00
2017-09-11 10:40:02 +02:00
## Teachers
2017-09-11 10:29:22 +02:00
2017-09-11 10:32:58 +02:00
* Functional Programming: Under the Hood (12h30, [François Pottier](http://gallium.inria.fr/~fpottier))
* Metatheory of Typed Programming Languages (12h30, [Didier Rémy](http://gallium.inria.fr/~remy/), *head*)
* Advanced Aspects of Type Systems (12h30, [Yann Régis Gianas](http://www.pps.jussieu.fr/~yrg/))
* Dependently-typed Functional Programming (12h30, [Pierre-Evariste Dagand](https://pages.lip6.fr/Pierre-Evariste.Dagand/))
2017-09-11 10:40:02 +02:00
## Aims
This course presents the principles and formalisms that underlie many of
today's typed functional programming languages.
The course is made up of four parts and can be split after the first two
parts.
In the first part, we discuss the *operational semantics* of functional
programming languages, and we present several classic *program
transformations*, including closure conversion, defunctionalization, and the
transformation into continuation-passing style (CPS). These program
transformations are interesting from two points of view. First, they are
*useful programming techniques*, which can help write or understand
programs. Second, they are used in the *compilation* of functional
programming languages, so they help understand what happens when the machine
executes a program. We use operational semantics to *prove* that the meaning
of programs is preserved by these transformations. Finally, we suggest how
these definitions and theorems can be expressed in a form that a machine can
check. That is, although Coq is not a prerequisite of the course, we will at
least try to *read and understand Coq definitions and statements*.
In the second part, we focus on the meta-theoretical properties of type
systems. We study parametric polymorphism (as in System F and ML), data
types and type abstraction. We show syntactic type soundness (via progress
and subject reduction) by reasoning by induction on typing derivations. We
also show how to obtain semantic properties via logical relations by
reasoning by induction on the structure of types. We also introduce
subtyping and row polymorphism and illustrate typing problems induced by
side effects (references) and the need for the value restriction.
The third part of the course describes more advanced features of type
systems: exceptions and effect handlers, including their typechecking and
static analyses: type inference, data flow and control flow analyses.
Finally, it introduces dependent types and refinement types.
The last part focuses on the use of dependent types for programming:
effectful programming with monads and algebraic effects; tagless
interpreters; programming with total functions; generic programming.
We also show the limits of dependently-typed functional programming.
## Approximate syllabus
### Functional Programming: Under the Hood
2017-09-11 10:41:47 +02:00
* (22/09/2017) From a small-step operational semantics...
* (29/09/2017) ... to an efficient interpreter. (2 weeks.)
* (06/10/2017) Compiling away first-class functions: closure conversion, defunctionalization.
* (13/10/2017) Compiling away the call stack: the CPS transformation.
* (20/10/2017) Equational reasoning and program optimizations.
2017-09-11 10:40:02 +02:00
### Metatheory of Typed Programming Languages
2017-09-11 10:43:57 +02:00
* (15/09/2017) Metatheory of System F. (Type soundness. Erasure.)
* (27/10/2017) ADTs, existential types, GADTs. (Typed program transformations.)
* (03/11/2017) Logical relations.
* (17/11/2017) Sub(typing. Rows. (Covariant arrays and covariant functions!)
* (24/11/2017) References. (Value restriction.)
2017-09-11 10:40:02 +02:00
### Advanced Aspects of Type Systems
2017-09-11 10:41:47 +02:00
* Exceptions and effect handlers. (Compiled away via CPS.)
* Typechecking exceptions and handlers.
* Type inference. (ML. Bidirectional. Elaboration.)
* Data/control flow analysis.
* Functional correctness. Intro to dependent/refinement types.
2017-09-11 10:40:02 +02:00
### Dependently-typed Functional Programming
2017-09-11 10:41:47 +02:00
* Effectful functional programming.
* Dependent functional programming.
* Total functional programming.
* Generic functional programming.
* Open problems in dependent functional programming.
2017-09-11 10:47:09 +02:00
## Recommended software
OCaml 4.0x and Coq **8.5**.
Once you have installed [opam](https://opam.ocaml.org/doc/Install.html), use the following commands:
```bash
opam init --comp=4.05 # for instance
opam repo add coq-released https://coq.inria.fr/opam/released
opam update
opam install -j4 -v coq.8.5.3
```
2017-09-11 10:50:20 +02:00
## Bibliography
[Types and Programming Languages](https://mitpress.mit.edu/books/types-and-programming-languages),
Benjamin C. Pierce, MIT Press, 2002.