Type Systems for Programming Languages

Login to KOS for course enrollment Display time-table
Code Completion Credits Range Language
PI-TPL ZK 4 0+3
Jan Vítek (guarantor)
Jan Vítek (guarantor)
Department of Theoretical Computer Science

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.

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.

Time-table for winter semester 2018/2019:
Time-table is not available yet
Time-table for summer semester 2018/2019:
Time-table is not available yet
The course is a part of the following study plans:
Data valid to 2019-03-20
For updated information see http://bilakniha.cvut.cz/en/predmet5083306.html