Type Systems for Programming Languages

Code 631
Semester Fall
Class Hours - Lab Hours 3 - 0
Lecturers Nikolaos Papaspyrou
Links Course's Website


This course studies the type systems that are used in modern programming languages. Through type systems, the main characteristics of imperative and functional programming languages are studied in depth: basic types, functions, recursion, references, exceptions, subtyping, recursive types, objects, polymorphism, existential and dependent types, types and logic. Emphasis is given to the contribution of type systems for the formal definition of programming languages and for studying safety properties of programs. Structural operational semantics is used as the vehicle for specifying the semantics of the languages under study. The students' evaluation is based on theoretical and practical assignments which are due throughout the semester.