I am a member of the School of Informatics at the university of Edinburgh. My main field of research lies in interactive theorem proving and its use in areas such as formalized mathematics and formal verification. I am particularly interested in the investigation of mathematical reasoning – both historical and contemporary – using proof assistants.
PhD in Formal Modelling and Verification for Healthcare: Are you interested in applying formal methods to real-world healthcare processes? If so, contact me. Funding may be available for good students.
PhD in Collaborative Theorem Proving: As part of the ProofPeer initiative, I am interested in supervising students on the application of machine learning and social computation to collaborative theorem proving. Funding may be available for good students. If this sounds like something you’d like to be involved in, get in touch!
Some of my latest research:
- I am the Principal Investigator for ProofPeer, an EPSRC-funded project on Collaborative Theorem Proving.
- Formal verification for healthcare, with an emphasis on the modelling of computer- and human-based processes and their interactions. More information is available here.
- I am (on and off) working on the formal reconstruction in the theorem prover Isabelle of proofs from Euler‘s famous Introductio in analysin infinitorum (Introduction to the Analysis of the Infinite), first published in 1748.
- Obua S., Scott P. and Fleuriot J. (2016). ProofScript: Proof Scripting for the Masses. To appear in Proceedings of ICTAC 2016, Springer LNCS.
- Manataki A., Fleuriot J. and Papapanagiotou P. (2016) A workflow-driven, formal methods approach to the generation of structured checklists for intra-hospital patient transfers. To appear in the Journal of Biomedical and Health Informatics.
- Scott P. and Fleuriot J. (2016). Compass-free Navigation of Mazes. EPiC Series in Computing, Volume 39, 143-155.
- Fleuriot J. and Ida T. (Eds., 2015). Geometric Reasoning. Special Issue of the Annals of Mathematics and Artificial Intelligence, Volume 74, Issue 3-4, Springer.
- Obua S., Fleuriot J., Scott P., and Aspinall D. (2015). Type Inference for ZFH. Proceedings of the International Conference on Intelligent Mathematics (CICM 2015), Springer LNCS, Volume 9150, 87-101.