B012511 - FOUNDATIONS OF PROGRAMMING LANGUAGES

Italian

Knowledge acquired:
Core topics in Programming Languages, including functional and object-oriented models.

Competence acquired (upon successful completion of this course).
Students will be able to formally define semantics and type systems for core languages, to study extensions to new constructs, to use formal techniques for proving languages and program properties, to design and implement type-checking algorithms, to use main contsruct of advanced languages in a suitable way.

Skills acquired.
1) A type-theoretic perspective to issues concerning language design, extensions and implementations.
2) Skills on using formal techniques for proving program properties.
3) A sufficient in depht introduction (to semantics and types) to understand the research literature on these topics.

Fundamental definitions and results in the theory of programming languages: operational semantics and associated formal proof , type systems. Functional languages and higher order functions, simple and polimorphic types. Subtyping in object-oriented languages. Tye-checking algorithms. Implementation issues.

Courses on formal methods are recommended. A solid programming experience is required.

We incorporate active learning strategies into every component of the course design.
Therefore we integrate different teaching methods:

a) Lectures
b) Development of in-class exercises

c) Assignments and Seminars by students. Each student, or group of 2-3 students, will be assigned a specific topic to study in depth; then they will give a presentation in class and lead the discussion on the given assignment.

There will be a final oral exam for each student.
The final mark will be determined by a weighted average of the scores on the final exam and the group-assignment with seminar.The percentage breakdown (roughly and subject to change) is 40% assignment and seminar, 60% final exam.

The course introduces core concepts and techniques in the foundational study of programming languages, as well as their formal logical underpinnings. Operational semantics and advanced type systems are studied with respect to major applications in software engineering, language design and security issues. A main goal is pragmatism: considering several programming languages (such as C++, Java and Python), language features are compared with practical motivations, including safety properties and type-checking algorithms.

Main topics.
1) Mathematical preliminars: induction and proof methods.
2) Operational semantics: introduction to structural rules. Introduction to type systems: decidability. References, assignment and store.
3) Programming with functions: Simply typed lambda-calculus. Strict and lazy semantics. Recursion. Evaluation strategies. Extensions. Types for higher-order functions. Type-safety proof.
4) Polymorphic types: Subtyping and relates algoritms. Universal types and type-reconstruction. Type-checking.
5) Case study: Featherweight Java (a core Java). Generic types. Type-safety. Intersection types andwildcard.
6) Functional programming: ML vs Python,static and dynamic type-checking, infinte data structures.
7) Lambda expressions in Java8 : typing problems.
8)Application: comparison of concrete languages (Java,C++ , Python, Haskell) with respect to main features induced by semantics and types.

Required textbook:
Types and Programming Languages, Benjamin C. Pierce.
The MIT Press, Cambridge, Massachusetts.
http://mitpress.mit.edu
ISBN 0-262-16209-1
Supplemental material, consisting of research papers, will be provided and covered in assignments and exams.

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 .