Type Systems for Programming Languages
Code | Completion | Credits | Range | Language |
---|---|---|---|---|
PI-TPL | ZK | 4 | 3C | English |
- Course guarantor:
- Jan Vitek
- Lecturer:
- Jan Vitek
- Tutor:
- Jan Vitek
- Supervisor:
- Department of Theoretical Computer Science
- Synopsis:
-
A type system is a static method for imposing constraints on legal programs in
order to guarantee their safe execution, which would prevent some class of
execution errors prior to running the program, whilst a semantics specifies what the
program will do when executed. Type systems in languages like Java and C#
provide a lightweight tool for identifying syntactic errors as well as erroneous uses
of data and illegal memory accesses.
More sophisticated type systems can be used to guarantee a multitude of other
properties, including reasoning about memory management and resource usage,
confidentiality and integrity of data, atomicity in concurrent programs, safe
execution of untrusted code.
This course gives an introduction to the main ideas and methodologies behind type
systems and semantics, and a practical exploration of typed features for commonly
used statically typed programming languages.
This course will be assessed through written assignments and a final project that
involves programming.
- Requirements:
- Syllabus of lectures:
-
Types of programming languages
* Untyped and simplytyped
lambda calculus.
* Small step and big step semantics.
* Type soundness. Progress and preservation theorems.
* Reference types and exceptions.
* Subtyping, inclusion, and coercion.
* Case study: Featherweight Generic Java.
Formal semantics of programming languages
* Principles of operational, denotational, and axiomatic semantics.
* Key concepts of semantics: compositionality, adequacy, observational
equivalence, full abstraction, and definability.
Practical statically typed programming languages
* Java: parametric polymorphism, generics, and wildcard semantics.
* Rust: object lifetime semantics and trait system.
* Standard ML language/OCaml/Haskell.
* Racket/Typed Racket
- Syllabus of tutorials:
- Study Objective:
-
This course will introduce students to the basic vocabulary and techniques
associated with type systems, and provide a taste of real world types system in
several highly regarded general purpose programming languages.
- Study materials:
-
Benjamin C. Pierce. Types and Programming Languages.
- Note:
- Time-table for winter semester 2024/2025:
- Time-table is not available yet
- Time-table for summer semester 2024/2025:
- Time-table is not available yet
- The course is a part of the following study plans:
-
- Informatics (doctoral) (compulsory elective course)
- Informatics (compulsory elective course)