th'>
st'>
D. Sangiorgi'>
]>
Typage 2017-18
Typage
M2PRO, anneé 2017-18
Last update: 16&th; Mar 2018
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
- All material in slides by Delia
- All material my slides, in particular (but not only)
- How to define functions as fixed-points (think of fact...)
- Kleene fixed point theorem, Knaster-Tarski theorem
- Coinductive definition of equivalence for closed recursive types
- How to convert inference rules into functions and vice versa
- Inference rules for subtyping (sections 21.3 and 21.8 TAPL)
- How to use them inductively and coinductively
- How to prove that two types are equivalent (i.e. coinduction proof method)
- Type rules for equi-recursive types
- Examples of type derivations with the above rules
Material
- Reference book
- [TAPL] Types and Programming Languages, B.C. Pierce
- Knaster-Tarski and fixed-points
-
- [TAPL] Chapter 21, or
this paper
- A lattice-theoretical fixpoint theorem and its applications, A. Tarski
- Reactive Systems, L. Aceto, A. Ingólfsdóttir, Theorem 4.1 (the proof is very clear).
- Introduction to Bisimulation and Coinduction,
&davide;, Chapter 3
- The Formal Semantics of Programming Languages, G. Winskell, Section 5.5
- Trees
- 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
- History...
-
- Mathematical Logic as Based on the Theory of Types,
B. Russell, 1908
- A formulation of the Simple Theory of Types,
A. Church, 1940
- Using category theory to design implicit conversions and generic operators,
J.C. Reynolds, 1980
- Advanced Topics in Bisimulation and Coinduction,
&davide; and J. Rutten (editors), Chapter 1