Oh no, Thomas Streicher, who was a great friend and mentor to me, passed way yesterday. Thomas was always very supportive (though often skeptical in a mentoring way), and brought me to Darmstadt, where I spent six wonderful years. He’s known for finding, with the also late Martin Hofmann, the groupoid model of Martin-Löf type theory. He saw it as a nonstandard model, but it paved the way for homotopy type theory and univalent mathematics. I will miss him dearly!
=> More informations about this toot | More toots from buchholtz@mathstodon.xyz
@buchholtz The first and only time I met Thomas was in September 2019 for the Workshop on Continuity, Computability, Constructivity (CCC) in Ljubljana. I was only a first-year PhD student and earlier that year at TYPES I had felt a little out of place at times, but Thomas immediately made me feel very comfortable. I have very few pictures of that trip, but the one attached captures exactly what I remember most: that it was very fun to talk with Thomas.
We made some tentative plans for me to visit him, but unfortunately, and partly because of the pandemic, I never followed up on these plans.
We are fortunate that he's left us with great expository notes on categorical logic, and realizability, as well as his book on domain-theoretic semantics of functional programming, all of which I have found very useful.
=> More informations about this toot | More toots from de_Jong_Tom@mathstodon.xyz
text/geminiThis content has been proxied by September (3851b).