Research interests:
 Computational Logic and Declarative Programming Languages,
 Automated and Interactive Provers,
 Higherorder Intercative Theorem Provers and Coq in particular;
 Induction and Coinduction, Recursion and Corecursion in logic and functional programming,
 Logic Programming, especially its Corecursive dialects,
 Logic Programming in Type Inference,
 Categorical Logic and Categorical Semantics of Computations,
 Coalgebraic semantics of logic programming,
 Proof Theory and Sequent Calculi,
 Applications of Statistical Machine Learning in Formal methods and Computational Logic.
Current Research grants:
 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 (HeriotWatt), S. Colton, J. Gow (Goldsmiths College).
Grant period: 01/11/15 to 31/10/19.
Previous Research grants (as a PI):
EPSRC grant Coalgebraic Logic Programming for Type Inference: parallelism and corecursion for a
new generation of programming languages, 20132017. Joint with John Power, University of Bath.
SICSA Industrial "Proof of Concept" grant
MachineLearning for Industrial Theorem Proving, 20132014. Joint with Jonathan Heras.

EPSRC First Grant scheme; project title
MachineLearning
Coalgebraic Automated Proofs, 20122014.
Associated with this grant is the project on ML4PG, on data mining proofs in Coq via Proof General interface.

EPSRC Postdoctoral Research Fellowship in Theoretical Computer Science; project title and webpage Computational Logic in Artificial Neural Networks, 20082011.
Smaller research grants, in parallel to the above:
 July 2017. Isaac Newton Institute (Cambridge) invited visitor at Big Proof research initiative.
 April 2013. SICSA workshop grant for ``Automated Reasoning Workshop" ARW'13, 1112 April 2013, University of Dundee.
 April 2013. British Logic Colloquium workshop grant for ARW'13.
 June 2011. SICSA Workshop grant for organisation of the workshop``Scottish Theorem Proving",
University of Dundee, 12 June 2011.

JulyAugust 2010, School of Computing, U. of Dundee. SICSAfunded grant ``Distinguished Academic Visitor",
for Dr John Power, Bath, UK.
 October 2009, School of Computer Science, University of St Andrews. Coauthor of the SICSAfunded grant ``Distinguished Academic Visitor",
for Prof. KaiUwe Kuehnberger, Osnabrueck, Germany.
 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 SophiaAntipolis, 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 higherorder proof assistant Coq.
My Postdoc was entitled Automatic Proofs for Recursive and Corecursive 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.