I am the Director of the Centre for Intelligent Systems and their Applications, which is part 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 Verification of Machine Learning Algorithms:  I am interested in supervising PhD students who wish to explore the foundations of machine learning (including Deep Learning), via formal verification. Candidates will need to have a strong  background in mathematics, an interest in computational logic/theorem proving and some experience in machine learning. Funding may be available for good applicants.

PhD in Formalised Mathematics for Physics: I am looking for research students interested in  the logical formulation and formalization of foundational aspects of (central) theoretical physics. Funding may be available for good students. Drop me an email, if you’re interested.

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: 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 currently working on various concepts related to the notion of Collaborative Mechanical 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 also 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.

 Recent Working Papers:

  • Papapanagiotou P. and Fleuriot J. (2018). Correct by Construction Resource-based Process Composition. CoRR abs/1803.02613
  • Obua S., Scott P. and Fleuriot J. (2017). Local Lexing. CoRR abs/1702.03277.
  • Scott P., Obua S. and Fleuriot J. (2017). Compiling Purely Functional Structured Programs. CoRR abs/1703.05227.
  • Fleuriot J., Obua S. and Scott P. (2016). Social Network Processes in the Isabelle and Coq Theorem Proving Communities.  CoRR abs/1609.07127

Latest Refereed Publications:

  • Narboux J., Janicic P. and Fleuriot J. (2018). Computer-assisted Theorem Proving in Synthetic Geometry. Chapter to appear in the
    Handbook of Geometric Constraint Systems Principles, Chapman and Hall/CRC.
  • Papapanagiotou P. and Fleuriot J. (2017). WorkflowFM:  A Logic-based Formal Verification Framework for Process Specification and Composition. To appear in the Proceedings of the 26th International Conference on Automated Deduction (CADE 26).
  • Dewanti A., Papapanagiotou P., Gilhooly C., Manataki A., Moss L. and Fleuriot J.  (2017). Development of Workflow-based Guidelines for the Care of Burns in Scotland. Proceedings of the 9th International Conference on e-Health. In press.
  • Alexandru C-A., Clutterbuck D., Papapanagiotou P., Fleuriot J. and Manataki A. (2017). A Step Towards the Standardisation of HIV Care Practices, 10th International Conference on Health Informatics. In press.

Comments are closed.