From ea28092e576e0f8ba2bcf019c24c62aa8abc55a4 Mon Sep 17 00:00:00 2001 From: Yann Regis-Gianas Date: Fri, 1 Dec 2017 09:50:23 +0100 Subject: [PATCH] Update part 3 syllabus. --- README.md | 26 ++++++++++++++++---------- 1 file changed, 16 insertions(+), 10 deletions(-) diff --git a/README.md b/README.md index eebc21b..8900d4a 100644 --- a/README.md +++ b/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 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 third part of the course introduces "rich" type systems designed +to guarantee extra properties in addition to safety: principality, +information hiding, modularity, extensionality, purity, control of +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: 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) -### Advanced Aspects of Type Systems +### Rich types, tractable typing -* 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. +* Type inference +* Subtyping +* Effects and resources +* Modules +* Dependent types +* Functional correctness ### Dependently-typed Functional Programming