A programming language should have a precise definition. Its behavior can be defined through grammatical and semantical rules. The former come from formal language theory, the latter from type theory and formal semantics, all independent areas of theoretical computer science.
In this undergraduate seminar we study the formal theory required to understand formally programming languages.
The goal of this seminar is to learn the fundamental concepts of programming languages, and understand the formal aspects and proof techniques of types systems and semantics. Being able to present a mathematically coherent account of the subject, and handle questions, is another important goal.
One shall acquire how a type is defined, and how to prove basic properties such as type soundness. Understanding various semantics and their applications.
