Worked as programmer in the 80s, studied computing in the 90s, Lecturer/researcher 2000-2020. Retire from paid work 2021, not from actual work.

Interests include program refinement (taught Event B, Ada, TLA+, CSP) and formal methods. I view the operational semantics as an excellent bridge between a wide range of formalisms. Add to this a small variant of Hennessy's Testing semantics and the application of Galois connections and you can glue together apparently different formalisms. This way I believe you can construct a very flexible yet rigorous definition of program refinement.

Had a lot of fun building a tool to model check the theory (yes the theory) and now am looking at embedding these ideas into Isabelle. You have to keep busy when you retire!

Personal view is Theoreticians can learn a lot from Engineers. Show bug to a compiler writer, they thank you and correct it. Show a bug to a theoretician and they hate you or look the other way. Theory will develop more quickly when we adopt good software engineering practice. Developing the theory and the executable tests together makes theory refactoring less problematic.