Update part 3 syllabus.
This commit is contained in:
parent
61142fa289
commit
ea28092e57
1 changed files with 16 additions and 10 deletions
26
README.md
26
README.md
|
@ -50,10 +50,15 @@ reasoning by induction on the structure of types. Finally, we introduce
|
||||||
subtyping, row polymorphism, and illustrate the problems induced by
|
subtyping, row polymorphism, and illustrate the problems induced by
|
||||||
side effects (references) and the need for the value restriction.
|
side effects (references) and the need for the value restriction.
|
||||||
|
|
||||||
The third part of the course describes more advanced features of type
|
The third part of the course introduces "rich" type systems designed
|
||||||
systems: exceptions and effect handlers, including their typechecking and
|
to guarantee extra properties in addition to safety: principality,
|
||||||
static analyses: type inference, data flow and control flow analyses.
|
information hiding, modularity, extensionality, purity, control of
|
||||||
Finally, it introduces dependent types and refinement types.
|
effects, algorithmic invariants, complexity, resource usage, or full
|
||||||
|
functional correctness. The expressivity of these systems sometimes
|
||||||
|
endangers the tractability, or even the feasibility, of type checking
|
||||||
|
and type inference: a common thread between these lectures discusses
|
||||||
|
the tradeoffs made on the design of these systems to balance
|
||||||
|
expressivity and tractability.
|
||||||
|
|
||||||
The last part focuses on the use of dependent types for programming:
|
The last part focuses on the use of dependent types for programming:
|
||||||
effectful programming with monads and algebraic effects; tagless
|
effectful programming with monads and algebraic effects; tagless
|
||||||
|
@ -131,13 +136,14 @@ We also show the limits of dependently-typed functional programming.
|
||||||
* See exercises in [course notes](http://gallium.inria.fr/~remy/mpri/cours.pdf)
|
* See exercises in [course notes](http://gallium.inria.fr/~remy/mpri/cours.pdf)
|
||||||
|
|
||||||
|
|
||||||
### Advanced Aspects of Type Systems
|
### Rich types, tractable typing
|
||||||
|
|
||||||
* Exceptions and effect handlers. (Compiled away via CPS.)
|
* Type inference
|
||||||
* Typechecking exceptions and handlers.
|
* Subtyping
|
||||||
* Type inference. (ML. Bidirectional. Elaboration.)
|
* Effects and resources
|
||||||
* Data/control flow analysis.
|
* Modules
|
||||||
* Functional correctness. Intro to dependent/refinement types.
|
* Dependent types
|
||||||
|
* Functional correctness
|
||||||
|
|
||||||
### Dependently-typed Functional Programming
|
### Dependently-typed Functional Programming
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue