Type theory, 7.5 credits

About the education

The course provides an introduction to type theory with simple and dependent types, how it can be used to represent logical systems and proofs, and how proofs give rise to computable functions. The final part of the course covers applications of type theory. The following topics are covered:

Type theory: lambda calculus, contexts, forms of judgement, simple types, inductive types. Operational semantics: confluence and normalization. The Curry-Howard isomorphism. Martin-Löf type theory: dependent types, induction and elimination rules, identity types, universes. The Brouwer-Heyting-Kolmogorov interpretation of logic. Meaning explanations. Semantics of dependent types. Explicit substitution. Category theoretical models. One or more of the following areas of application of type theory are covered: homotopy theory, models for (constructive) set theory and proof assistants.

Subject: Mathematics

As a mathematical theory always implies that certain conclusions hold under certain given conditions, it can in principle say nothing about the physical reality. None the less mathematics has become an indispensable tool for a large number of subjects like astronomy, physics, chemistry, statistics and the technical sciences and in later times also for economy, biology, various social sciences and computor science.

The role of mathematics in the applied sciences is both to supply notions for exact and adequate formulations of empirical laws but also from these laws to derive consequences, which can be used to find better models of the reality one has to describe. These tasks have lately become more important.

Mathematics is in continual progress by intensive international research, new theories are created and already existing theories are simplified and augmented.

Area of interest: Science and Mathematics

Science and mathematics help us understand how the world around us is connected – from the origin and structure of the universe, to the development and function of humanity and all other organisms on earth.

Scientific knowledge makes it possible to critically examine the credibility of information in different areas of everyday life, society, and the media.

As a scientist or mathematician, you will be attractive on a large job market that covers all parts of society and includes everything from pure technology companies to environment and healthcare, as well as research.

Department responsible for education

Department of Mathematics (incl. Math. Statistics)