Research interests:
 Computational Logic and Declarative Programming Languages,
 Automated and Interactive Theorem Provers,
 Verification for AI: how to prove AI algorithms (e.g. learning in neural networks) correct and secure,
 AI for Verification: applications of statistical machine learning in theorem proving,
 Induction and Coinduction, Recursion and Corecursion in logic and functional programming,
 Categorical Logic and Categorical Semantics of Computations.
Current Research grants:
 UK Research Institute in Verified Trustworthy Software Systems (VETSS)funded research project CONVENER: Continuous Verification of Neural Networks. Funded as part of "Digital Security Through Verification" call. Grant holders: E.Komendantskaya and D.Aspinall, named RAs: Wen Kokke and Daniel Kienitz.
Grant period: 01/04/20  31/03/2021.
 National Cyber Security Center (NCSC)funded research project SecConNN: Neural Networks with Security Contracts  towards lightweight, modular security for neural networks. Funded as part of NCSC "Security for AI" call. Grant holders: E.Komendantskaya and D.Aspinall.
Grant period: 01/11/19  31/03/2020.
Previous Research grants (as a PI):
 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.
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:
 Spring 2019. SICSA grant for organising the first Scottish Summer School on Programming Languages and Verification.
 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.