Books

- Fleuriot, J. (2001). A Combination of Geometry Theorem Proving and Nonstandard Analysis, with Application to Newton’s Principia. Distinguished Dissertations Series, Springer.
- Ida T. and Fleuriot J. (Eds., 2013). Automated Deduction in Geometry, Lecture Notes in Artificial Intelligence, LNCS Volume 7993, Springer.
- 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.

Edited Proceedings

- Ida. T. and Fleuriot J. (2012). The 9th International Workshop on Automated Deduction in Geometry, Informatics Research Report, Edinburgh.
- Fleuriot, J., Hofner P., McIver A, and Smaill A. (2013). ATx’12/WInG’12: Joint Proceedings of the Workshops on Automated Theory eXploration and on Invariant Generation , 6th International Joint Conference on Automated Reasoning 2012, EasyChair Proceedings (EPiC volume 17).

Refereed Articles

- 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).
- 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.
- Papapanagiotou P., Dewani A., Manataki A., Fleuriot J., Gilhooly C., Moss L. (2016). Workflow modelling of burns care protocols. The 26th SICS Annual Scientific Meeting, Scottish Intensive Care Society.
- 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.
- Scott P. and Fleuriot J. (2016). Compass-free Navigation of Mazes. EPiC Series in Computing, Volume 39, 143-155.
- 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.
- Papapanagiotou P. and Fleuriot J. D. (2015). Modelling and implementation of correct by construction healthcare workflows. Proceedings of Process-oriented Information Systems in Healthcare (ProHealth’14), LNBIB 202, 28-39.
- Papapanagiotou P., Fleuriot J., Manataki A., Winter A., Nandwani R., Clutterbuck D. and Wilks D. (2014). Rigorous development of computer based Integrated Care Pathways for HIV patients. Proceedings of the Health Informatics Scotland Conference 2014.
- Manataki A., Fleuriot J. D., and Papapanagiotou P. (2014). Tracheostomy transfers: A case study in the application of formal methods to intra-hospital patient transfers. Proceedings of the 27th IEEE International Symposium on Computer-Based Medical Systems (CBMS 2014).
- Papapanagiotou P. and Fleuriot J. D. (2014). Formal Verification of Collaboration Patterns in Healthcare. Behaviour and Information Technology, 33 (12): 1278-1293.
- 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. In 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 the 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, 2011, Volume 6877/2011, 34-50, DOI: 10.1007/978-3-642-25070-5_2.
- Papapanagiotou, P. and Fleuriot, J. D. (2011). Formal verification of Web Services composition using Linear Logic and the pi-calculus. Proceedings of the 9th IEEE European Conference on Web Services (ECOWS 2011), 1 – 38, DOI: 10.1109/ECOWS.2011.18.
- Scott, P. and Fleuriot J. D. (2011). Composable Discovery Engines for Interactive Theorem Proving. Lecture Notes in Computer Science, 2011, Volume 6898/2011, 370-375, DOI: 10.1007/978-3-642-22863-6_28.
- Scott, P. and Fleuriot J. D. (2011). An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time. Lecture Notes in Computer Science, 2011, Volume 6877/2011, 182-200, DOI: 10.1007/978-3-642-25070-5_11.
- Papapanagiotou, P. and Fleuriot J. D. (2011). A theorem proving framework for the formal verification of Web Services Composition. Proceedings of the 7th International Workshop on Automated Specification and Verification of Web Systems, EPTCS 61, pages 1-17, DOI:
**10.4204/EPTCS.61**. - Wilson, S. and Fleuriot, J. D. and Smaill. A. (2010). Automation for Dependently Typed Functional Programming. Fundamenta Informaticae.
- Papapanagiotou, P. and Fleuriot J. D. (2010). A Isabelle-like Procedural Language for HOL Light. In Proceedings of LPAR 2010, LNCS.
- Meikle, L. and Fleuriot, J. D. (2010). Integrating Systems around the User: Combining Isabelle, Maple, and QEPCAD in the Prover’s Palette. In Proceedings of the User Interfaces for Theorem Provers Workshop, FLOC 2010.
- Meikle, L. and Fleuriot, J. D. (2010). Automation for Geometry in Interactive Theorem Provers. In Proceedings of PAAR, FLOC 2010.
- Scott, P. and Fleuriot, J. D. (2010). Idle Time Proofs in Geometry. Proceedings of Automated Deduction in Geometry (ADG 2010), TU Munich.
- Wilson, S. and Fleuriot, J. D. and Smaill. (2010). Inductive Proof Automation for Coq. Proceedings of the Second Coq Workshop, FLOC 2010.
- Meikle, L. and Fleuriot, J. D. (2008). Combining Isabelle and QEPCAD-B in the Prover’s Palette. In Intelligent Computer Mathematics, volume 5144 of Lecture Notes in Computer Science, pages 314-330.
- Meikle, L. and Fleuriot, J. D. (2008). Prover’s Palette: A user-centric approach to verification with Isabelle and QEPCAD-B. In Computer Aided Verification, CAV, volume 5123 of Lecture Notes in Computer Science, pages 309-313. Springer.
- Meikle, L. I. and Fleuriot, J. D. (2006). Mechanical theorem proving in computational geometry. In Automated Deduction in Geometry, volume 3763 of LNCS, pages 1-18. Springer-Verlag.
- Dixon, L. and Fleuriot, J. D. (2005). A proof-centric approach to mathematical assistants. Journal of Applied Logic: Towards Computer Aided Mathematics Systems, 4(4):505-532.
- Bundy, A., Dixon, L., Gow, J. and Fleuriot, J. D. (2005). Constructing induction rules for deductive synthesis proofs. In Electronic notes in Theoretical Computer Science: Constructive Logic for Automated Software Engineering, pages 3-21.
- Wilson, S. and Fleuriot, J. D. (2005). Combining dynamic geometry, automated geometry theorem proving and diagrammatic proofs. In Proceedings of the User Interfaces for Theorem Provers Workshop.
- Dixon, L. and Fleuriot, J. D. (2004). Higher order rippling in IsaPlanner. In Theorem Proving in Higher Order Logics, TPHOLs 2004, volume 3223 of LNCS, pages 83-98. Springer.
- Brak, R. L., Fleuriot, J. D. and McGinnis, J. (2004). Theorem proving for protocol languages. In Proceedings of the Second European Workshop on Multi-Agent Systems (EUMAS 2004).
- Dixon, L. and Fleuriot, J. D. (2003). IsaPlanner: A prototype proof planner in Isabelle. In Proceedings of the 19th International Conference on Automated Deduction, CADE, volume 2741 of LNCS, pages 279-283.
- Meikle, L. I. and Fleuriot, J. D. (2003). Formalizing Hilbert’s grundlagen in Isabelle/Isar. In Theorem Proving in Higher Order Logics: 16th International Conference, TPHOLs 2003, volume 2758 of Lecture Notes in Computer Science, pages 319-334.
- Maclean, E., Fleuriot, J. and Smaill, A. (2002). Proof-planning non-standard analysis. In Proceedings of the Seventh International Symposium on Artificial Intelligence and Mathematics, Fort Lauderdale, Florida.
- Fleuriot, J. D. (2001). Theorem proving in infinitesimal geometry. Logic Journal of the IGPL, 9(3):471-498.
- Heneveld, A., Maclean, E., Bundy, A., Fleuriot, J. and Smaill, A. (2001). Solving integrals at the method level. In Kerber, M. and Kohlhase, M., (eds.), Symbolic Computation and Automated Reasoning, pages 251-252.
- Fleuriot, J. D. (2001). Nonstandard geometric proofs. In Wang, D. and Richter-Gebert, J., (eds.), Automated Deduction in Geometry, volume 2061, pages 238260. A shorter version appeared in the published in Proceedings of ADG 2000, pages 259-279, Zurich, Switzerland.
- Fleuriot, J. D. and Paulson, L. C. (2000). Mechanizing nonstandard real analysis. LMS Journal of Computation and Mathematics, 3(14):140-190.
- Fleuriot, J. D. (2000). On the mechanization of real analysis in Isabelle/HOL. In Harrison, J. and Aagaard, M., (eds.), Theorem Proving in Higher Order Logics: 13th International Conference,TPHOLs 2000, volume 1869 of Lecture Notes in Computer Science, pages 146-162. Springer-Verlag.
- Fleuriot, J. D. and Paulson, L. C. (1999). Proving Newton’s Propositio Kepleriana using geometry and nonstandard analysis in Isabelle. In Automated Deduction in Geometry 1998, volume 1669 of Lecture Notes in Artificial Intelligence, pages 47-66.
- Fleuriot, J. D. and Paulson, L. C. (1998). A combination of nonstandard analysis and geometry theorem proving, with application to Newton’s Principia. In Proceedings of the Fifteenth International Conference on Automated Deduction, CADE, volume 1421.

In Limbo

- Wilson, S. and Fleuriot, J. D. Geometry Explorer: Combining dynamic geometry, automated geometry theorem proving and diagrammatic proofs. To appear in: Electronic Notes in Theoretical Computer Science (Camera ready version submitted but awaiting to be published as a UITP special issue since 2006!).