- Computational Logic and Declarative Programming Languages,
- Automated and Interactive Provers,
- Higher-order 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 (Heriot-Watt), 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, 2013-2017. Joint with John Power, University of Bath.
SICSA Industrial "Proof of Concept" grant
Machine-Learning for Industrial Theorem Proving, 2013-2014. Joint with Jonathan Heras.
EPSRC First Grant scheme; project title
Coalgebraic Automated Proofs, 2012-2014.
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 web-page Computational Logic in Artificial Neural Networks, 2008-2011.
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, 11-12 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.
July-August 2010, School of Computing, U. of Dundee. SICSA-funded grant ``Distinguished Academic Visitor",
for Dr John Power, Bath, UK.
- 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.
- 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.
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.