- 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 SecCon-NN: 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 (Heriot-Watt), 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, 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:
- 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, 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.