Startseite > Fachgruppen > Softwaretechnik > Lehre > Type Systems for Correctness and Security SS2020

Type Systems for Correctness and Security SS2020

Course number and language

L.079.05814

The teaching language will be English. Questions in German will be permitted.

Course material

The slides and exercise sheets will be uploaded after each lecture on the course's PANDA page for the course. You should be automatically added if you are properly registered in PAUL. Let me know if this is not the case.

Registering and asking questions

To attend the course, you have to register in the PAUL system as a participant. To ask questions, please use the discussion forum in PANDA, so that others can benefit from the answers as well.

Time and Place

Wed 10:00-12:30 online according to the priority list in PANDA. Lecture recordings are available.

Exercise sessions will not take place currently. We will take critical things into the lecture stream and discuss everything else in Panda.

Abstract

Type systems in programming languages prevent illicit behavior of programs from the very start. They provide valuable feedback for programmers to prevent bugs, crashes or even security vulnerabilities. In this lecture we will study the theory, the properties and the implementation of modern type systems. 

Prerequisites

The course "Foundations of Programming Languages / Grundlagen der Programmiersprachen" is highly recommended but not required. In general you should be comfortable with formal, mathematical definitions as well as programming in Java, Scala, or a functional programming language.

Syllabus

We will cover the following topics (but are not limited to them):

  • Static vs. dynamic type checking
  • Operational semantics
  • Soundness of type systems
  • Type inference
  • Polymorphism
  • Subtyping
  • Security and safety guarantees through type systems
  • Path-dependent types
  • Dependent types 

We will take a pragmatic view on type systems and will develop type checkers along our way in this course to put theory into practice immediately. We will also take a closer look at type systems of well-known programming languages like Java or Scala.

Recommended reading material

The course is based on the following book:
Benjamin C. Pierce. 2002. Types and Programming Languages. The MIT Press.

We might cover some more advanced topics from this book:
Benjamin C. Pierce. 2004. Advanced Topics in Types and Programming Languages. The MIT Press. 

Other reading material will be announced on the course slides.