Email Gateway (Jan 13 2023 at 15:37): Email Gateway (Jan 13 2023 at 15:37):From: "\"Blanchette, J.C. (Jasmin Christian)\"" <cl-isabelle-users@lists.cam.ac.uk>
Dear Michael,
Since Andreas Abel has failed to deliver the goods, we agreed today that it is better to give the dependent type theory part of Chapter 3 to someone else.
Assia and I propose to give it to Jannis Limperg, a fourth-year PhD student of mine. He's an excellent writer (as can be seen from his CPP 2021 and 2023 papers) and understands DTT well enough to author these parts -- he worked with both Agda and Lean. Fun fact: He did his MSc with Andreas. Since he's more junior, he'd have more time to dedicate to this and his CV would benefit more from this. Also, I know from experience that he has a can-do attitude and will meet the deadline (we're aiming at end of June).
The plan would be that he adds a section about DTT at the end of your text. But you could discuss together what's the best way to integrate his contributions into your text.
I tentatively asked Jannis and he would be in, and he would, but of course this is all conditional on your agreement. Do you agree to work with Jannis? Or do you want to talk to him first?
Have a nice weekend.
Jasmin
Email Gateway (Jan 13 2023 at 15:39):From: "\"Blanchette, J.C. (Jasmin Christian)\"" <cl-isabelle-users@lists.cam.ac.uk>
Dear mailling list,
Please ignore my previous email. Somehow my email client auto-completed "Michael Norrish" to this mailing list!!
Terribly sorry again for the spam.
Best
Jasmin
Email Gateway (Jan 13 2023 at 16:29):From: Asta Halkjær From <andro.from@gmail.com>
Please don't apologise! As coauthor of that CPP 2023 paper, I think Jannis
deserves more public praise.
Asta
Last updated: Jan 04 2025 at 20:18 UTC