Jump to content

Thomas Streicher

From Wikipedia, the free encyclopedia

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 [de] 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]
  1. ^ Awodey, Steve (2010). "Type Theory and Homotopy". arXiv:1010.1810 [math.CT].
[edit]