Research interests:

  1. Computational Logic and Declarative Programming Languages,
  2. Automated and Interactive Theorem Provers,
  3. Verification for AI: how to prove AI algorithms (e.g. learning in neural networks) correct and secure,
  4. AI for Verification: applications of statistical machine learning in theorem proving,
  5. Induction and Coinduction, Recursion and Corecursion in logic and functional programming,
  6. Categorical Logic and Categorical Semantics of Computations.

Current Research grants:

Previous Research grants (as a PI):

  1. The Integration and Interaction of Multiple Mathematical Reasoning Processes. EPSRC Platform Grant EP/N014758/1 Grant holders: A. Ireland (PI), D. Aspinall, A. Bundy, A. Smaill, J. Fleuriot, P. Jackson (Edinburgh), G. Michaelson, K. Komedantskaya, Fiona McNeill (Heriot-Watt), S. Colton, J. Gow (Goldsmiths College). Grant period: 01/11/15 to 31/10/19.
  2. EPSRC grant Coalgebraic Logic Programming for Type Inference: parallelism and corecursion for a new generation of programming languages, 2013-2017. Joint with John Power, University of Bath.

  3. SICSA Industrial "Proof of Concept" grant Machine-Learning for Industrial Theorem Proving, 2013-2014. Joint with Jonathan Heras.

  4. EPSRC First Grant scheme; project title Machine-Learning Coalgebraic Automated Proofs, 2012-2014.

    Associated with this grant is the project on ML4PG, on data mining proofs in Coq via Proof General interface.

  5. EPSRC Postdoctoral Research Fellowship in Theoretical Computer Science; project title and web-page Computational Logic in Artificial Neural Networks, 2008-2011.

Smaller research grants, in parallel to the above:

  1. Spring 2019. SICSA grant for organising the first Scottish Summer School on Programming Languages and Verification.
  2. July 2017. Isaac Newton Institute (Cambridge) invited visitor at Big Proof research initiative.
  3. April 2013. SICSA workshop grant for ``Automated Reasoning Workshop" ARW'13, 11-12 April 2013, University of Dundee.
  4. April 2013. British Logic Colloquium workshop grant for ARW'13.
  5. June 2011. SICSA Workshop grant for organisation of the workshop``Scottish Theorem Proving", University of Dundee, 12 June 2011.
  6. July-August 2010, School of Computing, U. of Dundee. SICSA-funded grant ``Distinguished Academic Visitor", for Dr John Power, Bath, UK.
  7. October 2009, School of Computer Science, University of St Andrews. Co-author of the SICSA-funded grant ``Distinguished Academic Visitor", for Prof. Kai-Uwe Kuehnberger, Osnabrueck, Germany.
  8. 2005 -- 2007, Department of Mathemaics, University College Cork: Royal Society/Royal Irish Academy grant ``Category theory for natural models of computation'', PIs: Dr John Power, Laboratory for Foundations of Computer Science, University of Edinburgh, UK, and Dr Anthony Seda, Department of Mathematics, University College Cork, Ireland.

INRIA Postdoctoral experience

I did my first postdoc in INRIA Sophia-Antipolis, France. For 13 months, I had a pleasure to be a member of the Research Team Marelle. Marelle is one of the world's leading research units for development of automated higher-order proof assistant Coq. My Postdoc was entitled Automatic Proofs for Recursive and Co-recursive Formal Descriptions of Algorithms. PI: Yves Bertot. Funded by INRIA CORDI Fellowship Scheme.

PhD Thesis

I did my PhD at the Department of Mathematics,
University College, Cork (UCC), Ireland.

My PhD thesis is entitled Learning and Deduction in Neural Networks and Logic, 2007.