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

# Typage

## 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
• All material in slides by Delia
• All material my slides, in particular (but not only)
1. How to define functions as fixed-points (think of fact...)
2. Kleene fixed point theorem, Knaster-Tarski theorem
3. Coinductive definition of equivalence for closed recursive types
4. How to convert inference rules into functions and vice versa
5. Inference rules for subtyping (sections 21.3 and 21.8 TAPL)
6. How to use them inductively and coinductively
7. How to prove that two types are equivalent (i.e. coinduction proof method)
8. Type rules for equi-recursive types
9. Examples of type derivations with the above rules
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
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...
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