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

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.

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

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

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