Institute for Web Science and Technologies · Universität Koblenz - Landau
Institute WeST

What is a type system?

[zur Übersicht]
Martin Leinberger

Type systems are the most popular formal method of software engineering for ensuring that a system behaves correctly with regard to some specification. One informal definition of a (static) type system might be: “A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kind of values they compute”. In this talk, we will explore this definition through an example in order to better understand what a type system really is, the kind of errors it prevents and how it does that. The talk is based on the book “Types and Programming Languages” by Benjamin C. Pierce.

24.09.15 - 10:15
B 016