Welcome to my webpage!

I am a Professor in Computer Science (AI and Verification) at the School of Mathematical and Computer Sciences (MACS), Heriot-Watt University

I do research on logic, programming languages, verification and AI. I lead the Lab for AI and Verification

My recent and upcoming events:

2020:

Grants:

• Research project AISEC: AI Secure and Explainable by Construction, is starting in September 2020. Funded as part of "Security for All in AI Enabled Society" call. Grant holders: E.Komendantskaya, D.Aspinall, B.Atkey, V.Rieser, B.Schafer.
• Research project CONVENER: Continuous Verification of Neural Networks started in April 2020. Funded by UK Research Institute in Verified Trustworthy Software Systems (VETSS) as part of "Digital Security Through Verification" call. Grant holders: E.Komendantskaya and D.Aspinall, named RAs: Wen Kokke and Daniel Kienitz.

Invited talks:

• Continuous Verification of AI: a Declarative Programming Approach at PPDP'20, the 22nd International Symposium on Principles and Practice of Declarative Programming.
• AI Verification, in Need of Programming Language Support at the SICSA annual conference.
• Refinement types for Verification of Neural Networks at the Workshop on Program Semantics, Specification and Verification (PSSV).

Research papers:

• Neural Networks, Secure by Construction: An Exploration of Refinement Types. (joint with Wen Kokke, Daniel Kienitz, Robert Atkey, and David Aspinall) APLAS'20, the The 18th Asian Symposium on Programming Languages and Systems .
• The New Normal: We Cannot Eliminate Cuts in Coinductive Sequent Calculi, But We Can Explore Them (joint with Dmitry Rozplokhas and Henning Basold) ICLP'20, the 36th International Conference on Logic Programming.
• Proof-Carrying Plans: a Resource Logic for AI Planning (joint with Alasdair Hill and Ron Petrick) has been accepted for publication in PPDP'20, the 22nd International Symposium on Principles and Practice of Declarative Programming.
• Research abstract Robustness as a Refinement Type: Verifying Neural Networks in Liquid Haskell and F*. (joint with Wen Kokke, Daniel Kienitz and David Aspinall), ETAPS Workshop LiVe'20: 4th Workshop on Learning in Verification, 25 April 2020, Dublin, Ireland
• Relative Robustness of Quantized Neural Networks Against Adversarial Attacks (joint with Kirsty Duncan, Robert Sewart, Michael Lones) the International Joint Conference on Neural Networks, IJCNN'20, 19-24 July 2020, Glasgow, Scotland.
• Accuracy, Training Time and Hardware Efficiency Trade-Offs for Quantized Neural Networks on FPGAs. (joint with Pascal Bacchus and Robert Stewart) accepted at the 16th International Symposium on Applied Reconfigurable Computing 2020 (ARC2020), 1-3 April Toledo, Spain.

Conference Chairing:

• PC Chair of the 22nd Symposium on Practical Aspects of Declarative Languages (PADL'20) , co-allocated with POPL'20 in New Orleans, in January 2020.
• PC chair of TEASE-LP 2020: Trends, Extensions, Applications and Semantics of Logic Programming, Dublin, Ireland, co-located with ETAPS 2020 on 25 April 2020.
• Co-ognaiser of the the 2nd Scottish Summer School on Programming languages and Verification (SPLV), Edinburgh, August 2020.

PC membership:

• PC member at the Certified Programs and Proofs at POPL'21, 17 - 22 January 2021 Copenhagen, Denmark.
• PC member at the The 36th International Conference on Logic Programming (ICLP 2020) Rende, Italy, 18-24 September 2020 .
• PC member at the The miniKanren and Relational Programming Workshop Jersey City, New Jersey, United States, 23 - 28 August 2020 .
• PC member at the 29th International Conference on Artificial Neural Networks (ICANN'20).
• PC member at the International Joint Conference on Neural Networks (IJCNN 2020) Glasgow, UK, 19-24 July 2020.
• PC member at the 15th IFIP WG 1.3 International Workshop on Coalgebraic Methods in Computer Science (CMCS 2020), Dublin, Ireland, 25 - 26 April 2020.
• PC member at the 15th International Symposium on Functional and Logic Programming (FLOPS 2020) , 23-25 April, 2020, Akita, Japan.
• Steering Committee member for the 22nd International Symposium on Principles and Practice of Declarative Programming, PPDP'20.
• PC member of the 23rd Symposium on Practical Aspects of Declarative Languages (PADL'21), co-allocated with POPL'21
• PC member of the Logic in Computer Science (LICS) conference in 2021.

My selected publications (full list is given here):

• Wen Kokke, Ekaterina Komendantskaya, Daniel Kienitz, Robert Atkey, and David Aspinall. Neural Networks, Secure by Construction: An Exploration of Refinement Types. In APLAS'20, the The 18th Asian Symposium on Programming Languages and Systems.
• E.Komendantskaya, D. Rozplokhas, H. Basold The New Normal: We Cannot Eliminate Cuts in Coinductive Sequent Calculi, But We Can Explore Them. ICLP'20, the 36th International Conference on Logic Programming.
• H. Basold, E. Komendantskaya, Y. Li Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses. ESOP 2019 (28th European Symposium on Programming), 8-11 April 2019, Prague.
• C.Schwaab, E.Komendantskaya, A.Hill, F.Farka, J.Wells, R.Petrick, K.Hammond. Proof-Carrying Plans. PADL 2019, 14-15 January 2019, Cascais/Lisbon, Portugal.
• E.Komendantskaya and J.Power Logic Programming: Laxness and Saturation. Journal of Logical and Algebraic Methods in Programming Volume 101, December 2018, Pages 1-21.
• E.Komendantskaya and J.Heras Proof Mining with Dependent Types, Conference on Intelligent Computer Mathematics, CICM'17 in Edinburgh, 17-21 July 2017, Edinburgh.
• P.Fu, E.Komendantskaya, T.Schrijvers, A.Pond. Proof Relevant Corecursive Resolution Thirteenth International Symposium on Functional and Logic Programming FLOPS'2016, Japan, 3-6 March 2016. Springer LNCS 9613, 126-143.
• E.Komendantskaya, J.Power and M.Schmidt. Coalgebraic Logic Programming: from Semantics to Implementation. Journal of Logic and Computation, 26(2), 745-783, 2016.
• J.Heras, E.Komendantskaya, M.Johansson, and E.Maclean. Proof-Pattern Recognition and Lemma Discovery in ACL2 19th International conference on Logic for Programming Artificial Intelligence and Reasoning, LPAR'13, Stellenbosch, South Africa, 15-19 December 2013. Springer LNCS 8312, pp. 389-406, 2013.
• Y. Bertot and E. Komendantskaya. Inductive and Coinductive Components of Corecursive Functions in Coq, CMCS'08, the 9th International Workshop on Coalgebraic Methods in Computer Science, Budapest, Hungary, 4 - 6 April, 2008. ENTCS 203/5 pp.25--47, 2008.