- Docente: Simone Martini
- Credits: 6
- SSD: INF/01
- Language: Italian
- Teaching Mode: Traditional lectures
- Campus: Bologna
- Corso: Second cycle degree programme (LM) in Computer Science (cod. 8028)
Learning outcomes
At the end of the course, the student
knows the main type systems of programming languages, including
universal and existential polymorphism, subtypes, recursive types,
and techiques for type inference. In particular, he will be able to
derive the principal type of a term and understand whether the type
defined for a term is correct.
Course contents
Types and programming languages. Typed lambda-calculus as analysis and design tool. Simple types, ML-polynorphism. Type inference and its complexity. Subtypes. Recursive types: maximal fixed point, coinduction and their role in subtyping definition. Higher types. Generics and their description. Abstract data types and existential types. Proof carrying code.
Readings/Bibliography
Benjamin Pierce, Types and
Programming Languages, The MIT Press (ISBN
0-262-16209-1)
Teaching methods
Lectures
Assessment methods
Oral examination.
Teaching tools
http://www.cs.unibo.it/~martini/TLP/index.html
Links to further information
http://www.cs.unibo.it/~martini/TLP/index.html
Office hours
See the website of Simone Martini