Course teached as: B012511 - TEORIA DEI LINGUAGGI DI PROGRAMMAZIONE Second Cycle Degree in COMPUTER SCIENCE
Teaching Language
Italian
Course Content
Fundamental techniques, concepts and results in the theory of programming languages. Main topics are operational semantics and type systems, wich define both the style of programming and the formal properties of programs.
Types and Programming Languages. Benjamin C. Pierce. MIT Press, 2002.
Learning Objectives
At the end of the course, students should have acquired the following competences:
1) A rigorous approach, based on type theory, the study of problems related to the design of languages, their extensions and implementations.
2) Ability to use formal techniques to try to study the properties of the programs.
3) A preparation sufficiently deep (on semantics and types) to allow the deepening of research publications on the topics discussed.
Number of hours for personal study and other individual learning: 90
Number of hours for classroom activities: 48
Number of hours for seminars to: 12
Further information
Attendance to lectures: strongly recommended.
Teaching Tools UNIFI E-Learning: https://e-l.unifi.it/.
Office Hours: by appointment.
Contact the teacher by e-mail: venneri@unifi.it .
Type of Assessment
Activities of seminars by students. Final oral examination.
Course program
1) Mathematical preliminars: induction and proof methods.
2) Operational semantics: introduction to structural rules. Introduction to type systems: decidability. References, assignment and store.
2) Programming with functions: Simply typed lambda-calculus. Strict and lazy semantics. Recursion. Evaluation strategies. Extensions. Types for higher-order functions. Type-safety proof.
3) Polymorphic types: Subtyping and relates algoritms. Universal types and type-reconstruction. Type-checking.
3) Case study: Featherweight Java (a core Java). Generic types. Type-safety. Intersection types andwildcard.
4) Functional programming: ML vs Python,static and dynamic type-checking, infinte data structures.
4) Lambda expressions in Java8 : typing problem