Thomas Streicher

Last updated

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.

Mathematics field of study concerning quantity, patterns and change

Mathematics includes the study of such topics as quantity, structure, space, and change.

Technische Universität Darmstadt university

The Technische Universität Darmstadt, commonly referred to as TU Darmstadt, is a research university in the city of Darmstadt, Germany. It was founded in 1877 and received the right to award doctorates in 1899. In 1882 it was the first university in the world to set up a chair in electrical engineering, and founded the first faculty for it in 1883. Nobel laureate Albert Einstein once recommended this university. TU Darmstadt's alumni include 2 Nobel laureates and 2 Leibniz Prize winners.

The University of Passau is a public research university located in Passau, Lower Bavaria, Germany. Founded in 1973, it is the youngest university in Bavaria and consequently has the most modern campus in the state. Nevertheless, its roots as the Institute for Catholic Studies date back some hundreds of years.



His research interests include categorical logic, domain theory and Martin-Löf type theory.

Categorical logic is the branch of mathematics in which tools and concepts from category theory are applied to the study of mathematical logic. It is also notable for its connections to theoretical computer science. In broad terms, categorical logic represents both syntax and semantics by a category, and an interpretation by a functor. The categorical framework provides a rich conceptual background for logical and type-theoretic constructions. The subject has been recognisable in these terms since around 1970.

Domain theory is a branch of mathematics that studies special kinds of partially ordered sets (posets) commonly called domains. Consequently, domain theory can be considered as a branch of order theory. The field has major applications in computer science, where it is used to specify denotational semantics, especially for functional programming languages. Domain theory formalizes the intuitive ideas of approximation and convergence in a very general way and has close relations to topology.

In joint work with Martin Hofmann he constructed a model for intensional Martin-Löf type theory where identity types are interpreted as groupoids. This was the first model with non-trivial identity types, i.e. other than sets. Based on this work [1] other models with non-trivial identity types were studied, including homotopy type theory which has been proposed as a foundation for mathematics in Vladimir Voevodsky's research program Univalent Foundations of Mathematics.

Set (mathematics) fundamental mathematical concept related to the notions of belonging or inclusion

In mathematics, a set is a collection of distinct objects, considered as an object in its own right. For example, the numbers 2, 4, and 6 are distinct objects when considered separately, but when they are considered collectively they form a single set of size three, written {2, 4, 6}. The concept of a set is one of the most fundamental in mathematics. Developed at the end of the 19th century, set theory is now a ubiquitous part of mathematics, and can be used as a foundation from which nearly all of mathematics can be derived. In mathematics education, elementary topics from set theory such as Venn diagrams are taught at a young age, while more advanced concepts are taught as part of a university degree.

Homotopy type theory

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

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.

Together with Martin Hofmann he received the 2014 LICS Test-of-Time Award for the paper "The groupoid model refutes uniqueness of identity proofs".


International Standard Book Number Unique numeric book identifier

The International Standard Book Number (ISBN) is a numeric commercial book identifier which is intended to be unique. Publishers purchase ISBNs from an affiliate of the International ISBN Agency.

Related Research Articles

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.

In mathematics, homotopy groups are used in algebraic topology to classify topological spaces. The first and simplest homotopy group is the fundamental group, which records information about loops in a space. Intuitively, homotopy groups record information about the basic shape, or holes, of a topological space.

Intuitionistic type theory is a type theory and an alternative foundation of mathematics. Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician and philosopher, who first published it in 1972. There are multiple versions of the type theory: Martin-Löf proposed both intensional and extensional variants of the theory and early impredicative versions, shown to be inconsistent by Girard's paradox, gave way to predicative versions. However, all versions keep the core design of constructive logic using dependent types.

In mathematics, the Seifert–van Kampen theorem of algebraic topology, sometimes just called van Kampen's theorem, expresses the structure of the fundamental group of a topological space in terms of the fundamental groups of two open, path-connected subspaces that cover . It can therefore be used for computations of the fundamental group of spaces that are constructed out of simpler ones.

In mathematics, a setoid is a set X equipped with an equivalence relation ~. A Setoid may also be called E-set, Bishop set, or extensional set.

Per Martin-Löf Swedish logician, philosopher, and mathematical statistician

Per Erik Rutger Martin-Löf is a Swedish logician, philosopher, and mathematical statistician. He is internationally renowned for his work on the foundations of probability, statistics, mathematical logic, and computer science. Since the late 1970s, Martin-Löf's publications have been mainly in logic. In philosophical logic, Martin-Löf has wrestled with the philosophy of logical consequence and judgment, partly inspired by the work of Brentano, Frege, and Husserl. In mathematical logic, Martin-Löf has been active in developing intuitionistic type theory as a constructive foundation of mathematics; Martin-Löf's work on type theory has influenced computer science.

Constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory. That is, it uses the usual first-order language of classical set theory, and although of course the logic is constructive, there is no explicit use of constructive types. Rather, there are just sets, thus it can look very much like classical mathematics done on the most common foundations, namely the Zermelo–Fraenkel axioms (ZFC).

The ACM–IEEE Symposium on Logic in Computer Science (LICS) is an annual academic conference on the theory and practice of computer science in relation to mathematical logic. Extended versions of selected papers of each year's conference appear in renowned international journals such as Logical Methods in Computer Science and ACM Transactions on Computational Logic.

Rudolf Wille German Mathematician

Rudolf Wille was a German mathematician and was professor of General Algebra from 1970 to 2003 at Technische Universität Darmstadt. His most celebrated work is the invention of formal concept analysis, an unsupervised machine learning technique that applies mathematical lattice theory to organize data based on objects and their shared attributes.

Ulrich Kohlenbach German mathematician

Ulrich Wilhelm Kohlenbach is a German professor of mathematics and a researcher in logic. His research interests lie in the field of proof mining.

In mathematics, especially (higher) category theory, higher-dimensional algebra is the study of categorified structures. It has applications in nonabelian algebraic topology, and generalizes abstract algebra.

In mathematics, directed algebraic topology is a refinement of algebraic topology for directed spaces, topological spaces and their combinatorial counterparts equipped with some notion of direction. Some common examples of directed spaces are spacetimes and simplicial sets. The basic goal is to find algebraic invariants that classify directed spaces up to directed analogues of homotopy equivalence. For example, homotopy groups and fundamental n-groupoids of spaces generalize to homotopy monoids and fundamental n-categories of directed spaces. Directed algebraic topology, like algebraic topology, is motivated by the need to describe qualitative properties of complex systems in terms of algebraic properties of state spaces, which are often directed by time. Thus directed algebraic topology finds applications in Concurrency, Network traffic control, General Relativity, Noncommutative Geometry, Rewriting Theory, and Biological systems.

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.

In mathematics, especially in higher-dimensional algebra and homotopy theory, a double groupoid generalises the notion of groupoid and of category to a higher dimension.

Ronald Brown (mathematician) British mathematician

Ronald Brown is an English mathematician. Emeritus Professor in the School of Computer Science at Bangor University, he has authored many books and more than 160 journal articles.

Univalent foundations are an approach to the foundations of mathematics in which mathematical structures are built out of objects called types. Types in the 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 the "categorical" mathematics in the style of Alexander Grothendieck. It departs from the use of predicate logic as the underlying formal deduction system, replacing it, at the moment, by a version of the Martin-Löf type theory. The development of the univalent foundations is closely related with 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. Awodey, Steve (2010). "Type Theory and Homotopy". arXiv: 1010.1810 Lock-green.svg.

The Mathematics Genealogy Project is a web-based database for the academic genealogy of mathematicians. By 13 February 2019, it contained information on 238,725 mathematical scientists who contributed to research-level mathematics. For a typical mathematician, the project entry includes graduation year, thesis title, alma mater, doctoral advisor, and doctoral students.