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 (algebra), space (geometry), and change. It has no generally accepted definition.

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. In 1883, the university founded the first faculty of electrical engineering and introduced the world's first degree course in electrical engineering. In 2004, it became the first German university to be declared as an autonomous university.

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.

Contents

Work

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 well-defined 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.

Homotopy type theory variant of type theory incorporating the univalence axiom of Voevodsky

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.

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".

Bibliography

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. 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.

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 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.

Thomas Weiland is a German physicist, engineer and university lecturer. He is Professor of Electrical Engineering at the Technische Universität Darmstadt in Germany. He was named a Fellow of the Institute of Electrical and Electronics Engineers (IEEE) in 2012 for his development of the finite integration technique and impact of the associated software on electromagnetic engineering.

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.

References

  1. Awodey, Steve (2010). "Type Theory and Homotopy". arXiv: 1010.1810 .

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.