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.
Some of my latest research:
- I am 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.
- Formal verification for healthcare, with an emphasis on the modelling of collaborative work.
- I am also involved in ProofPeer, a project on Collaborative Theorem Proving.
Latest Refereed Publications
- Papapanagiotou P. and Fleuriot J. D. (2013). Formal Verification of Collaboration Patterns in Healthcare. To appear in Behaviour and Information Technology.
- Meikle L. I. and Fleuriot J. D. (2012): Integrating Systems around the User: Combining Isabelle, Maple, and QEPCAD in the Prover’s Palette. Electr. Notes Theor. Comput. Sci. 285: 115-119.
- Scott, P. and Fleuriot, J. D. (2012) . Towards a Synthetic Proof of the Polygonal Jordan Curve Theorem. Proceedings of the Automated Deduction in Geometry workshop (ADG 2012), 147-156.
- Scott, P. and Fleuriot, J. D. (2012). A Combinator Language for Theorem Discovery. In Proceedings of the Conferences on Intelligent Computer Mathematics (CICM 2012), Lecture Notes in Computer Science, Volume 7362, 371-385, DOI:10.1007/978-3-642-31374-5_25.
- Papapanagiotou, P., Fleuriot, J. D., and Grando A. (2012). Rigorous process-based modelling of patterns for collaborative work in healthcare teams. In Proceedings of the 25th IEEE International Symposium on Computer-Based Medical Systems (CBMS 2012), DOI: 10.1109/CBMS.2012.6266330.
- Papapanagiotou, P., Fleuriot, J. D. , and Wilson, S. (2012). Diagrammatically-driven formal verification of web-services composition. In Proceedings of Diagrams 2012 conference, Lecture Notes in Computer Science Volume 7352, 241-255, DOI: 10.1007/978-3-642-31223-6_25.
- Fleuriot, J. D. (2011). Exploring the Foundations of Discrete Analytical Geometry in Isabelle/HOL. Lecture Notes in Computer Science, Volume 6877/2011, 34-50, DOI: 10.1007/978-3-642-25070-5_2.