Thorsten Altenkirch

Last updated

Thorsten Altenkirch
Alma mater University of Edinburgh
Scientific career
Fields Constructive mathematics
Type theory
Homotopy type theory
Institutions University of Nottingham
Institute for Advanced Study
Doctoral advisor Rod Burstall

Thorsten Altenkirch (German pronunciation: [ˈtɔʁstn̩ ˈʔaltn̩kɪʁç] ) is a German Professor of Computer Science at the University of Nottingham [1] known for his research on logic, type theory, and homotopy type theory. Altenkirch was part of the 2012/2013 special year on univalent foundations at the Institute for Advanced Study. [2] At Nottingham he co-chairs the Functional Programming Laboratory with Graham Hutton.

Germany Federal parliamentary republic in central-western Europe

Germany, officially the Federal Republic of Germany, is a country in Central and Western Europe, lying between the Baltic and North Seas to the north and the Alps, Lake Constance and the High Rhine to the south. It borders Denmark to the north, Poland and the Czech Republic to the east, Austria and Switzerland to the south, France to the southwest, and Luxembourg, Belgium and the Netherlands to the west.

University of Nottingham university in Nottingham, United Kingdom

The University of Nottingham is a public research university in Nottingham, United Kingdom. It was founded as University College Nottingham in 1881, and was granted a royal charter in 1948.

In mathematics, logic, and computer science, a type theory is any of a class of formal systems, some of which can serve as alternatives to set theory as a foundation for all mathematics. In type theory, every "term" has a "type" and operations are restricted to terms of a certain type.



Altenkirch obtained his PhD from the University of Edinburgh under Rod Burstall. [3]

University of Edinburgh public research university in Edinburgh, Scotland

The University of Edinburgh, founded in 1582, is the sixth oldest university in the English-speaking world and one of Scotland's ancient universities. The university has five main campuses in the city of Edinburgh, with many of the buildings in the historic Old Town belonging to the university. The university played an important role in leading Edinburgh to its reputation as a chief intellectual centre during the Age of Enlightenment, and helped give the city the nickname of the Athens of the North.

Rodney Martineau "Rod" Burstall FRSE is a British computer scientist and one of four founders of the Laboratory for Foundations of Computer Science at the University of Edinburgh.


Altenkirch's work includes: Containers, Epigram programming language, and Homotopy Type Theory: Univalent Foundations of Mathematics (The HoTT Book).

In type theory, containers are abstractions which permit various "collection types", such as lists and trees, to be represented in a uniform way. A (unary) container is defined by a type of shapes S and a type family of positions P, indexed by S. The extension of a container is a family of dependent pairs consisting of a shape and a function from positions of that shape to the element type. Containers can be seen as canonical forms for collection types.

Epigram is a functional programming language with dependent types. Epigram also refers to the IDE usually packaged with the language. Epigram's type system is strong enough to express program specifications. The goal is to support a smooth transition from ordinary programming to integrated programs and proofs whose correctness can be checked and certified by the compiler. Epigram exploits the propositions as types principle, and is based on intuitionistic type theory.

Altenkirch has also been a guest on the YouTube channel Computerphile [4]

Related Research Articles

Set theory Branch of mathematics that studies sets

Set theory is a branch of mathematical logic that studies sets, which informally are collections of objects. Although any type of object can be collected into a set, set theory is applied most often to objects that are relevant to mathematics. The language of set theory can be used to define nearly all mathematical objects.

Vladimir Voevodsky Russian mathematician

Vladimir Alexandrovich Voevodsky was a Russian-American mathematician. His work in developing a homotopy theory for algebraic varieties and formulating motivic cohomology led to the award of a Fields Medal in 2002. He is also known for the proof of the Milnor conjecture and motivic Bloch-Kato conjectures and for the univalent foundations of mathematics and homotopy type theory.

Institute for Advanced Study postgraduate center in Princeton, New Jersey

The Institute for Advanced Study (IAS), located at 1 Einstein Drive, Princeton, New Jersey, in the United States, is an independent postdoctoral research center for theoretical research and intellectual inquiry. It was founded in 1930 by American educator Abraham Flexner, together with philanthropists Louis Bamberger and Caroline Bamberger Fuld.

J. H. C. Whitehead British mathematician

John Henry Constantine Whitehead FRS, known as Henry, was a British mathematician and was one of the founders of homotopy theory. He was born in Chennai, in India, and died in Princeton, New Jersey, in 1960.

In computer science, a function type is the type of a variable or parameter to which a function has or can be assigned, or an argument or result type of a higher-order function taking or returning a function.

The vertical bar ( | ) is a computer character and glyph with various uses in mathematics, computing, and typography. It has many names, often related to particular meanings: Sheffer stroke, verti-bar, vbar, stick, vertical line, vertical slash,bar, pike, or pipe, and several variants on these names. It is occasionally considered an allograph of broken bar.

André Joyal Canadian mathematician

André Joyal is a professor of mathematics at the Université du Québec à Montréal who works on category theory. He was a member of the School of Mathematics at the Institute for Advanced Study in 2013, where he was invited to join the Special Year on Univalent Foundations of Mathematics.

In programming languages and type theory, a product of types is another, compounded, type in a structure. The "operands" of the product are types, and the structure of a product type is determined by the fixed order of the operands in the product. An instance of a product type retains the fixed order, but otherwise may contain all possible instances of its primitive data types. The expression of an instance of a product type will be a tuple, and is called a "tuple type" of expression. A product of types is a direct product of two or more types.

In type theory, a system has inductive types if it has facilities for creating a new type along with constants and functions that create terms of that type. The feature serves a role similar to data structures in a programming language and allows a type theory to add concepts like numbers, relations, and trees. As the name suggests, inductive types can be self-referential, but usually only in a way that permits structural recursion.

ALF is a structure editor for monomorphic Martin-Löf type theory developed at Chalmers University. It is a predecessor of the Alfa, Agda, Cayenne and Coq proof assistants and dependently typed programming languages. It was the first language to support inductive families and dependent pattern matching.

In mathematics, the first Blakers–Massey theorem, named after Albert Blakers and William S. Massey, gave vanishing conditions for certain triad homotopy groups. This connectivity result may also be expressed as that if X is the pushout of

Conor McBride is a lecturer in the department of Computer and Information Sciences at the University of Strathclyde. In 1999 he completed a PhD in 'Dependently Typed Functional Programs and their Proofs' at the University of Edinburgh for his work in type theory. He previously worked at Durham University and briefly at Royal Holloway, University of London before joining the academic staff at the University of Strathclyde.

Homotopy type theory

In mathematical logic and computer science, homotopy type theory refers to various lines of development of intuitionistic type theory, based on the interpretation of types as objects to which the intuition of (abstract) homotopy theory applies.

Thomas Streicher is a Professor of Mathematics at Technische Universität Darmstadt. He received his PhD in 1988 from the University of Passau with advisor Manfred Broy.

In mathematics, equivalent definitions are used in two somewhat different ways. First, within a particular mathematical theory, a notion may have more than one definition. These definitions are equivalent in the context of a given mathematical structure. Second, a mathematical structure may have more than one definition.

Univalent foundations are an approach to the foundations of mathematics in which mathematical structures are built out of objects called types. Types in univalent foundations do not correspond exactly to anything in set-theoretic foundations, but they may be thought of as spaces, with equal types corresponding to homotopy equivalent spaces and with equal elements of a type corresponding to points of a space connected by a path. Univalent foundations are inspired both by the old Platonic ideas of Hermann Grassmann and Georg Cantor and by "categorical" mathematics in the style of Alexander Grothendieck. Univalent foundations depart from the use of classical predicate logic as the underlying formal deduction system, replacing it, at the moment, with a version of Martin-Löf type theory. The development of univalent foundations is closely related to the development of homotopy type theory.

Michael "Mike" Shulman is an American mathematician at the University of San Diego who works in category theory and higher category theory, homotopy theory, logic as applied to set theory, and computer science. He did his undergraduate work at the California Institute of Technology and his postgraduate work at the University of Cambridge and the University of Chicago, where he received his Ph.D. in 2009.

In type theory, a polynomial functor is a kind of endofunctor of a category of types that is intimately related to the concept of inductive and coinductive types. Specifically, all W-types are initial algebras of such functors.


  1. "Thorsten Altenkirch".
  2. "Program Participants".
  3. Thorsten Altenkirch at the Mathematics Genealogy Project
  4. "Computerphile". YouTube. Retrieved 11 January 2017.