Research interests:

  1. Computational Logic and Declarative Programming Languages,
  2. Automated and Interactive Provers,
  3. Higher-order Intercative Theorem Provers and Coq in particular;
  4. Induction and Coinduction, Recursion and Corecursion in logic and functional programming,
  5. Logic Programming, especially its Corecursive dialects,
  6. Logic Programming in Type Inference,
  7. Categorical Logic and Categorical Semantics of Computations,
  8. Coalgebraic semantics of logic programming,
  9. Proof Theory and Sequent Calculi,
  10. Applications of Statistical Machine Learning in Formal methods and Computational Logic.

Current Research grants:

Previous Research grants (as a PI):

  1. 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.

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

  3. 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.

  4. 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. July 2017. Isaac Newton Institute (Cambridge) invited visitor at Big Proof research initiative.
  2. April 2013. SICSA workshop grant for ``Automated Reasoning Workshop" ARW'13, 11-12 April 2013, University of Dundee.
  3. April 2013. British Logic Colloquium workshop grant for ARW'13.
  4. June 2011. SICSA Workshop grant for organisation of the workshop``Scottish Theorem Proving", University of Dundee, 12 June 2011.
  5. July-August 2010, School of Computing, U. of Dundee. SICSA-funded grant ``Distinguished Academic Visitor", for Dr John Power, Bath, UK.
  6. 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.
  7. 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.