WikiMili The Free Encyclopedia

The topic of this article may not meet Wikipedia's general notability guideline .(February 2015) (Learn how and when to remove this template message) |

**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** includes the study of such topics as quantity, structure, space, and change.

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

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.

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

- T. Streicher (1991),
*Semantics of Type Theory: Correctness, Completeness, and Independence Results*, Birkhäuser Boston. ISBN 3764335947 - M. Hofmann and T. Streicher (1996), The groupoid interpretation of type theory, in Sambin, Giovanni (ed.) et al., Twenty-five years of constructive type theory. Proceedings of a congress, Venice, Italy, October 19–21, 1995.
- T. Streicher (2006),
*Domain-theoretic Foundations of Functional Programming*, World Scientific Pub Co Inc. ISBN 9812701427

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.

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

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

- Official website at Technische Universität Darmstadt
- Thomas Streicher at the Mathematics Genealogy Project

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.

This article about a German mathematician is a stub. You can help Wikipedia by expanding it. |

This page is based on this Wikipedia article

Text is available under the CC BY-SA 4.0 license; additional terms may apply.

Images, videos and audio are available under their respective licenses.

Text is available under the CC BY-SA 4.0 license; additional terms may apply.

Images, videos and audio are available under their respective licenses.