th'> st'> D. Sangiorgi'> ]> Typage 2017-18


M2PRO, anneé 2017-18

Last update: 16&th; Mar 2018

Jour Sujet
10-01-2018 par Delia
17-01-2018 par Delia
24-01-2018 par Delia
31-01-2018 par Delia
07-02-2018 Fixed points and recursive types
14-02-2018 Knaster-Tarski, coinduction and equi-recursion
21-02-2018 Functions and inference rules
28-03-2018 More on recursive types
07-02-2018 A type for Y: light introduction to intersection types
14-03-2018 Exercice au tableau
14-03-2018 Exercice au tableau

Examen: 28 Mars, 10h00 -- 12h00, salle 2035 bât. Sophie Germain
Documents autorisés: deux feuilles A4 manuscrites et strictement personelles.

Soutenance projet: jour, lieu ???
Modalité soutenance: exposé oral de ~15min sur le projet (en utilisant votre ordinateur), plus ~5 min de questions.

Syllabus Material
Reference book
[TAPL] Types and Programming Languages, B.C. Pierce
Knaster-Tarski and fixed-points
  1. [TAPL] Chapter 21, or this paper
  2. A lattice-theoretical fixpoint theorem and its applications, A. Tarski
  3. Reactive Systems, L. Aceto, A. Ingólfsdóttir, Theorem 4.1 (the proof is very clear).
  4. Introduction to Bisimulation and Coinduction, &davide;, Chapter 3
  5. The Formal Semantics of Programming Languages, G. Winskell, Section 5.5
Fundamental properties of infinite trees, B. Courcelle
Typing with equi-recursive types
Type inference with recursive types: Syntax and semantics, Section 1 and 2, F. Cardone, M. Coppo
Functions vs. inference rules
[TAPL] Chapter 21, or this paper
Intersection Types
Types with intersection: an introduction, J. R. Hindley
  1. Mathematical Logic as Based on the Theory of Types, B. Russell, 1908
  2. A formulation of the Simple Theory of Types, A. Church, 1940
  3. Using category theory to design implicit conversions and generic operators, J.C. Reynolds, 1980
  4. Advanced Topics in Bisimulation and Coinduction, &davide; and J. Rutten (editors), Chapter 1