Type Systems for Programming Languages

Garant předmětu:

Jan Vitek

Přednášející:

Jan Vitek

Cvičící:

Jan Vitek

Předmět zajišťuje:

katedra teoretické informatiky

Anotace:

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.

Požadavky:

Osnova přednášek:

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

Osnova cvičení:

Cíle studia:

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.

Studijní materiály:

Benjamin C. Pierce. Types and Programming Languages.

Poznámka:

Tento předmět je i pro české studenty POUZE v anglickém jazyce.

Rozvrh na zimní semestr 2024/2025:

Rozvrh není připraven

Rozvrh na letní semestr 2024/2025:

Rozvrh není připraven

Předmět je součástí následujících studijních plánů:

• Informatika (doktorská) (povinně volitelný předmět)
• Informatika (povinně volitelný předmět)