Jacques Carette (Dec 18 2020 at 16:33):
We're hiring! 8 new positions in CS/SE. All areas (even though the ad kind of tries to shy away from that, believe the first sentence).
We are very formal-friendly. Many of us already use theorem provers in our daily work. We'd love more. Jeff Zucker is still here, even though he's retired; he did his PhD formalizing Real Analysis in Automath in the early 1970s! And of course there's Bill Farmer too, co-author of IMPS. Wolfram Kahl and I are quite active around Agda. Mark Lawford uses PVS a fair bit. Others use model checkers, and so on.
Your main work should have a definite CS/SE flavour though. We are called "Computing & Software", after all.
Last updated: Aug 03 2023 at 10:10 UTC