Type Systems for Programming Languages
Kód | Zakončení | Kredity | Rozsah | Jazyk výuky |
---|---|---|---|---|
PI-TPL | ZK | 4 | 3C | anglicky |
- Garant předmětu:
- Jan Vitek
- Přednášející:
- 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)