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
His research interests include
Martin-Löf type theory
.
In joint work with
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
- 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
External links
- Official website at Technische Universität Darmstadt
- Thomas Streicher at the Mathematics Genealogy Project