The Tyranny of Types: Curse or Blessing?
Speaker | Sarah Tilscher, Anastasiia Izycheva |
Location | see schedule below |
Time | see schedule below |
Module | IN0014, IN2107 |
Content
Type systems play an essential role in the design of many programming languages. By classifying terms according to the kinds of values they compute, optimizations can be included, feedback can be provided to the programmer and certain run-time errors can be avoided. Beyond that, extended type systems have been proposed for program analyses on secure information-flow, resource usage or possible data races.
In this seminar we will examine a variety of type systems of modern programming languages and highlight some of their different concepts. In the course of that, we will discuss the advantages and limitations of static and dynamic type inference. Beyond that, we can take a look at some extended type systems that enable program analyses for other safety properties.
Schedule
The seminar will be organized as a mini-conference. After submitting your draft paper you will be asked to review some drafts of your fellow students. The received feedback should be incorporated before submitting the final version of the paper. The final talks will be held en-block within two or three days at the end of the semester.
Pre-course meeting | Feb 4th, 4pm | bbb.in.tum.de/sar-qtx-s7p-x1p |
Kick-off meeting | Mar 29th, 2pm | slides |
Topic distribution | until April 11th | |
Individual meetings to discuss literature choice and outline | tba | |
Draft paper submission | Jun 5th | LaTeX Template (we are using ACM Primary Article Template) |
Review submisson | Jun 19th | |
Final paper submission | July 3rd | |
Talks | July 14th and 15th, 9am - 3pm | 03.11.018 |
Topics
Topic | Reference Paper | |
Static vs Dynamic Typing | link | BA |
Gradual Typing | link | BA/MA |
Type Inference Algorithms | link | BA |
Union and Intersection Types | link | BA |
Type Classes | link | BA/MA |
Application of Refinement Types | link | BA/MA |
Generalized Algebraic Data Types (GADTs) | link | BA/MA |
Effect Systems | link | MA |
Ownership-based Types | link | MA |
Dependent Types | link | MA |
Liquid Types | link | BA/MA |
Path-Dependent Types | link | MA |
Type-Level Programming | link | MA |
Type-Guided Program Synthesis | link | MA |
Type Error Explanation | link | MA |
Using Types for Security | link | MA |
Report Template
Please use this LaTeX Template for your submissions (we are using ACM Primary Article Template). You only need to submit the resutling PDF.
If you cannot download our template you can apply the settings manually:
\documentclass[sigconf,review,svgnames,dvipsnames,nonacm]{acmart}
\acmConference[Types 2022]{The Tyranny of Types: Curse or Blessing?}{11 - 14 July, 2022}{Munich}
\setcopyright{none}
\copyrightyear{2022}
\acmYear{2022}
\acmPrice{0}
\bibliographystyle{ACM-Reference-Format}
\usepackage{amsmath}
Prerequesites
This seminar is open to Master and advanced Bachelor students. The following lectures are helpful (but not required) prerequisites for this course:
- Functional Programming and Verification
- Lambda Calculus
- Programming Languages
- Semantics of Programming Languages
- Compiler Construction