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.

Opportunities:

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:

  • 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:

  • 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.
  • Obua S., Scott P. and Fleuriot J. (2016). ProofScript: Proof Scripting for the Masses. International Colloquium on Theoretical Aspects of Computing, ICTAC 2016, Springer LNCS, Volume 9965, 333-348.
  • 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. The IEEE Journal of Biomedical and Health Informatics, Issue 99, 1-7.

Comments are closed.