 | ||
Books Semantics of type theory, Domain-theoretic Foundations of Functional Programming | ||
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.
Contents
Extra planetary experiences w author thomas streicher ph d
Work
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 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".