This course is an in-depth investigation of the theory of programming languages, covering the fundamental techniques for analysis, design and implementation of programming languages. Main topics: operational semantics and associated formal proofs ; higher-order functions, lambda calculus and partial evaluation; type systems and type-safety for functional and object- oriented paradigms; polymorphism; dynamic and static type-checking.
Required textbook: Types and Programming Languages. Benjamin C. Pierce. MIT Press, 2002.
Supplemental material, consisting of research papers, will be provided and covered in assignments and exams.
Learning Objectives
Upon successful completion of this course, a student will be able
- to formally define semantics and type systems for core languages, and to design extensions with new constructs
- to use formal techniques for proving properties of programs and languages
- to explain design concepts, key features, design alternatives and trade-offs, by comparing modern programming languages critically
- to choose a suitable programming language for a given problem
- to quickly become productive in a new language .
Prerequisites
Courses on formal methods are recommended. A solid programming experience is required.
Teaching Methods
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.
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
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, the group-assignment and the class participation. The percentage breakdown (roughly and subject to change) is 30% assignment and seminar, 65% final exam, and 5% participation (which includes attendance, participation in class and contribution to discussions).
Course program
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 subjects:
1)Type systems: simple types, metatheory of subtype, algorithms for static and dynamic type-checking, parametric polymorphism and type-reconstruction.
3) Three formal core languages.
a) Expressions and Imperative constructs
b) Featherweight Java , a core model of Java and object-oriented programming . Generics types. Formal proof of Safety. Intersection types and lambda expressions.
c) Lambda-calculus, a core model of functional programming languages. Type inference for functions. Several different evaluation strategies for function application and their consequences. Formal proof of Safety.
4) Application: comparison of concrete languages (Java,C++ , Python, Haskell) with respect to main features induced by semantics and types.
5) Safety mechanisms to model interactions among communicating systems. The formalism of Session Types to describe communications protocols, enabling dynamic verification: the protocols are implemented (and adapted) in order to avoid unexpected consequences, such as deadlocks.