Thomas Streicher
 | The topic of this article may not meet Wikipedia's notability guideline for academics. (February 2015) |
Thomas Streicher (born 1958) is an Austrian mathematician who 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.
Work
[edit]His research interests include categorical logic, domain theory and Martin-Löf type theory.
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.
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
[edit]- 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
References
[edit]- ^ Awodey, Steve (2010). "Type Theory and Homotopy". arXiv:1010.1810 [math.CT].
External links
[edit]- Official website at Technische Universität Darmstadt
- Thomas Streicher at the Mathematics Genealogy Project
| International | |
|---|---|
| National | |
| Academics | |
| Other | |
 | This article about a German mathematician is a stub. You can help Wikipedia by expanding it. |