Research Papers

    2023
  1. Natalia Slusarz, Ekaterina Komendantskaya, Matthew L. Daggitt, Robert J. Stewart, Kathrin Stark: Logic of Differentiable Logics: Towards a Uniform Semantics of DL. LPAR 2023, 24th International Conference on Logic for Programming, AI and Reasoning.
  2. Matthew L. Daggitt, Robert Atkey, Wen Kokke, Ekaterina Komandantskaya, Luca Arnaboldi. Compiling higher-order specifications to SMT solvers: how to deal with rejection constructively. Certified Proofs and Programs. CPP'23. Boston, USA, 16-17 January 2023.
  3. Remi Desmartin, Omri Isac, Grant O. Passmore, Kathrin Stark, Guy Katz, Ekaterina Komendantskaya: Towards a Certified Proof Checker for Deep Neural Network Verification. LOPSTR'2023, October 2023, Cascais, Portugal.
  4. Matthew Daggitt, Wen Kokke, Ekaterina Komendantskaya, Robert Atkey, Luca Arnaboldi, Natalia Slusarz, Marco Casadio, Ben Coke and Jeonghyeon Lee. The Vehicle Tutorial: Neural Network Verification with Vehicle. FOMLAS 2023: 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems Affiliated with CAV 2023. Easychair Proceedings.
  5. Marco Casadio, Luca Arnaboldi, Matthew L. Daggitt, Omri Isac, Tanvi Dinkar, Daniel Kienitz, Verena Rieser, Ekaterina Komendantskaya: ANTONIO: Towards a Systematic Method of Generating NLP Benchmarks for Verification. FOMLAS 2023: 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems Affiliated with CAV 2023 . Easychair Proceedings.
  6. Luca Arnaboldi, David Aspinall, Ronny Bogani, Burkhard Schafer, Scott Herman, Jonathan Protzenko, Ekaterina Komendantskaya, Yue Li , Remi Desmartin. Formalising Criminal Law in Catala. PRoLaLa, POPL Workshop on Programming Languages and the Law 2023
    7. 2022
  7. D. Kienitz, E. Komendantskaya and M. Lones. The Effect of Manifold Entanglement and Intrinsic Dimensionality on Learning. Thirty-Sixth AAAI Conference on Artificial Intelligence (AAAI22).
  8. M. Casadio, E. Komendantskaya, M. L. Daggitt, W. Kokke, G. Katz, G. Amir and I. Refaeli: Neural Network Robustness as a Verification Property: A Principled Case Study. International conference on Computer-Aided Verification CAV'22 (Part of FLOC'22).
  9. R. Desmartin, G. Passmore E. Komendantskaya and M. Daggitt: CheckINN: Wide Range Neural Network Verification in Imandra. 24th International Symposium on Principles and Practice of Declarative Programming PPDP'22.
  10. D. Kienitz, E. Komendantskaya and M. Lones. Comparing Complexities of Decision Boundaries for Robust Training: A Universal Approach. Asian Conference on Computer Vision, ACCV'22.
  11. M. Daggitt, W. Kokke, R. Atkey, L. Arnaboldi and E. Komendantskaya: Vehicle: A High-Level Language for Embedding Logical Specifications in Neural Networks. The 5th Workshop on Formal Methods for ML-Enabled Autonomous Systems (FoMLAS'22).
  12. N. Slusarz, E. Komendantskaya, M. Daggitt and R. Stewart: Differentiable Logics for Neural Network Verification. The 5th Workshop on Formal Methods for ML-Enabled Autonomous Systems (FoMLAS'22).
  13. M. Casadio, E. Komendantskaya, V. Rieser, M. Daggitt, D. Kienitz, L. Arnaboldi and W. Kokke: Why Robust Natural Language Understanding is a Challenge. The 5th Workshop on Formal Methods for ML-Enabled Autonomous Systems (FoMLAS'22).
  14. R. Desmartin, G. Passmore and E. Komendantskaya: Neural Networks in Imandra: Matrix Representation as a Verification Choice. The 5th Workshop on Formal Methods for ML-Enabled Autonomous Systems (FoMLAS'22).
    15. 2021
  15. R. Stewart, A. Nowlan, P. Bacchus, Q. Ducasse, E. Komendantskaya. Optimising Hardware Accelerated Neural Networks with Quantization and a Knowledge Distillation Evolutionary Algorithm. J. Electronics 10, 396 (2021).
  16. K.Duncan, R. Stewart and E.komendantskaya. Logically Constrained Pruning Towards RobustNeural Networks. 4th Workshop on Formal Methods for ML-Enabled Autonomous Systems (FOMLAS) (co-allocated with CAV21).
  17. A.Hill, E. Komendantskaya, M. Daggitt and R.Petrick. Actions You Can Handle:Dependent Types for AI Plans. The Workshop on Type-Driven Development 2021 (co-allocated with ICFP21).
    18. 2020
  18. 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.
  19. Alasdair Hill, Ekaterina Komendantskaya and Ron Petrick. Proof-Carrying Plans: a Resource Logic for AI Planning PPDP'20, the 22nd International Symposium on Principles and Practice of Declarative Programming.
  20. Ekaterina Komendantskaya, Dmitry Rozplokhas and Henning 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.
  21. Wen Kokke, Ekaterina Komendantskaya, Daniel Kienitz and David Aspinall. Robustness as a Refinement Type: Verifying Neural Networks in Liquid Haskell and F*. Accepted at ETAPS Workshop LiVe'20: 4th Workshop on Learning in Verification, 25 April 2020, Dublin, Ireland. See also SecCONN-NN project webpage
  22. Kirsty Duncan, Ekaterina Komendantskaya, Robert Sewart, Michael Lones Relative Robustness of Quantized Neural Networks Against Adversarial Attacks, accepted to be published and presented at the International Joint Conference on Neural Networks, IJCNN.20, part of the world congress on computational intelligence: https://wcci2020.org/ 19-24 July 2020, Glasgow, Scotland.
  23. P. Bacchus, R. Stewart, E. Komendantskaya. Accuracy, Training Time and Hardware Efficiency Trade-Offs for Quantized Neural Networks on FPGAs. 16th International Symposium on Applied Reconfigurable Computing 2020 (ARC2020), 1-3 April Toledo, Spain.
    24. 2019
  24. E. Komendantskaya, R. Stewart, K. Duncan, D. Kienitz, P. Le Hen, P. Bacchus Neural Network Verification for the Masses (of AI graduates). Experience report. 2019.
  25. 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.
  26. C.Schwaab, E.Komendantskaya, A.Hill, F.Farka, J.Wells, R.Petrick, K.Hammond. Proof-Carrying Plans. PADL 2019 (21st International Symposium on Practical Aspects of Declarative Languages), 14-15 January 2019, Cascais/Lisbon, Portugal.
    27. 2018
  27. E.Komendantskaya and J.Power. Logic programming: laxness and saturation. Journal of Logic and Algebraic Methods in Programming. 101: 1-21.
  28. F.Farka, E.Komendantskaya and H.Hammond Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis. International Conference on Logic Programming ICLP'18, FLoC'18, 14-17 July 2018, Oxford. Journal of Theory and Practice of Logic Programming, 18 (3-4): 484-501.
  29. A.Hill and E.Komendantskaya Automation by Analogy, in Coq. 3rd Conference on Artificial Intelligence and Theorem Proving AITP 2018 Aussois, France, 25 - 30 March 2018.
    30. 2017
  30. E.Komendantskaya and Y.Li Productive Corecursion in Logic Programming. International Conference on Logic Programming ICLP'17, 28-31 August 2017, Melbourne. Selected papers published in J. of Theory and Practice of Logic Programming TPLP 17(5-6): 906-923. 2017.
  31. P.Fu and E.Komendantskaya. Operational Semantics of Resolution and Productivity in Horn Clause Logic. Journal ``Formal Aspects of Computing", 29(3): 453-474, 2017. Project's webpage.
  32. E.Komendantskaya and J.Heras Proof Mining with Dependent Types, CICM'17 in Edinburgh, 17-21 July 2017, Edinburgh. LNCS 10383: 303-318, 2017.
  33. L.Franceschini, D.Ancona and E.Komendantskaya. Structural Resolution for Abstract Compilation of Object-Oriented Languages. Proceedings of the First Workshop on Coalgebra, Horn Clause Logic Programming and Types, CoALP-Ty 2016, Edinburgh, UK, 28-29 November 2016. EPTCS 258, 2017. See also MSc thesis of L.Franceschini, U.Genova, 2016.
    34. 2016
  34. E.Komendantskaya, J.Power and M.Schmidt. Coalgebraic Logic Programming: from Semantics to Implementation. Journal of Logic and Computation, 26(2), 745-783, 2016. CoALP's mini-page.
  35. F.Farka, E.Komendantskaya, K.Hammond and P.Fu. Coinductive Soundness of Corecursive Type Class Resolution. Pre- and post- proceedings of LOPSTR'16, Edinburgh, UK.
  36. E.Komendantskaya, P.Johann and M.Schmidt. A Productivity Checker for Logic Programming. Pre- and post- proceedings of LOPSTR'16, Edinburgh, UK.
  37. E.Komendantskaya and J.Power. Category theoretic semantics for theorem proving in logic programming: embracing the laxness. Coalgebaric methods in Computer Sceince (CMCS'16): Revised selected papers. Lecture Notes in Computer Science 9608, 94--113, 2016. Project's webpage.
  38. P.Fu, E.Komendantskaya, T.Schrijvers, A.Pond. Proof Relevant Corecursive Resolution FLOPS'2016, Japan, 3-6 March 2016. Springer LNCS 9613, 126-143. Project's webpage.
    39. 2015
  39. P.Fu and E.Komendantskaya. A Type Theoretic Approach to Resolution. LOPSTR 2015: Revised and Selected papers, Lecture Notes in Computer Science 9527, pages 91--106.
  40. C.Warburton and E. Komendantskaya Scaling Automated Theory Exploration. Workshop AI4FM, Edinburgh, 2015.
  41. E. Komendantskaya, P. Fu and P. Johann. Structural Resolution for Automated Verification, "Ideas paper"; 15th International Workshop on Automated Verification of Critical Systems AVOCS'15, Edinburgh. Project's webpage.
  42. P. Johann, E. Komendantskaya and V.Komendantskiy. Structural Resolution for Logic Programming. Technical Communications of ICLP 2015. Project's webpage.
  43. P.Fu and E.Komendantskaya. A Type Theoretic Approach to Structural Resolution. Pre-proceedings of LOPSTR 2015. Project's webpage.
    44. 2014
  44. J. Heras and E. Komendantskaya. Proof-Pattern Search in Coq/SSReflect. Proceedings Coq Workshop, FLoC 2014. Electronic Proceedings in Theoretical Computer Science, pp. 61-75, 2014.
  45. J. Heras and E. Komendantskaya. ACL2(ml): Machine-Learning for ACL2. Proceedings ACL2 Workshop, FLoC 2014.
  46. J.Heras, E.Komendantskaya and M.Schmidt. (Co)recursion in Logic Programming: Lazy versus Eager. Technical Communications of International Conference on Logic Programming (ICLP'14) at FLoC'14. Benchmarks for this paper. CoALP's mini-page.
  47. J.Heras, E.Komendantskaya, Recycling Proof Patterns in Coq: Case Studies. Mathematics in Computer Science 8(1): 99-116 (2014). Arxiv version. ML4PG page.
  48. E.Komendantskaya, M.Schmidt and J.Heras. Exploiting Parallelism in Coalgebraic Logic Programming. Electr. Notes Theor. Comput. Sci. 303: 121-148 (2014). CoALP's mini-page
    49. 2013
  49. J.Heras, E.Komendantskaya, M.Johansson, and E.Maclean. Proof-Pattern Recognition and Lemma Discovery in ACL2 LPAR'13, Stellenbosch, South Africa, 15th-19th December 2013. LNCS 8312, pp. 389-406, 2013.
  50. E.Komendantskaya, J.Heras and G.Grov. Machine-Learning for Proof General: interfacing interfaces. Post-proceedings of User Interfaces for Theorem Provers (UITP 2012), EPTCS, vol. 118, pp. 15-41, 2013. ML4PG has its own page: here.
  51. J.Heras and E.Komendantskaya. ML4PG in Computer Algebra Verification. Systems & Projects session of CICM 2013. Lecture Notes in Computer Science, vol. 7961, pp. 354-358, 2013. Arxiv version.
  52. J.Heras and E.Komendantskaya. Statistical Proof Pattern Recognition: Automated or Interactive? (slides), the 20th Automated Reasoning Workshop (ARW'13), 11-12 April 2013.
    53. 2012
  53. E.Komendantskaya, J.Power and M.Schmidt. Coalgebraic Logic Programming: implicit versus explicit resource handling. Workshop on Coinductive Logic Programming at ICLP'12, Budapest, September 2012. Slides are available here.
  54. E.Komendantskaya and K.Lichota. Neural Networks for Proof-Pattern Recognition. International Conference on Artificial Neural Networks, ICANN'12, September 2012, Lausanne, Switzerland. Lecture Notes in Computer Science, vol. 7553, pp. 427-434, 2012. The supporting documentation and data sets are available here.
  55. G.Grov, E.Komendantskaya and A.Bundy. A Statistical Relational Learning Challenge - extracting proof strategies from exemplar proofs. ICML'12 worshop on Statistical Relational Learning, Edinburgh, 30 July 2012.
  56. E.Komendantskaya. Machine-Learning Coalgebraic Proofs. Post-proceedings of the International Conference on Inductive Logic Programming'11, Windsor, UK. Imperial College Tech. Report.
    57. 2011
  57. E.Komendantskaya and Q.Zhang. SHERLOCK - An Inteface for Neuro-Symbolic Networks. NeSy version, longer version. The software package is available here. System presentation at NeSy'11 workshop at ECAI'11. CEUR Workshop Proceedings.
  58. E.Komendantskaya and J.Power. Coalgebraic derivations in logic programming. International conference Computer Science Logic, CSL'11. LIPICS proceedings, Vol 12, pp.352-366.
  59. E.Komendantskaya and J.Power. Coalgebraic semantics for derivations in logic programming. International conference on Algebra and Coalgebra CALCO'11. Springer LNCS 6859, pp. 268-282.
  60. E.Komendantskaya and J.Power. Coalgebraic proofs in logic programming. Proceedings of the 18th Workshop on Automated Reasoning, Dept of Computing Science, University of Glasgow (Tech Report), 2011.
    61. 2010
  61. A.Bove, E. Komendantskaya and M.Niqui. Proceedings of the PAR'10 workshop on Partiality and Recursion at FLoC'10. Edinburgh, UK. Electronic Proceedings in Theoretical Computer Science. 2010.
  62. E. Komendantskaya, K. Broda and A. d'Avila Garcez. Neuro-Symbolic Representation of Logic Programs Defining Infinite Sets. In K. Diamantaras, et al.(Eds.): ICANN 2010, Part I, LNCS 6352, Springer, pp.301-304.
  63. Ekaterina Komendantskaya, Guy McCusker and John Power. Coalgebraic semantics for parallel derivation strategies in logic programming. Proceedings of AMAST'2010 - 13th International Conference on Algebraic Methodology and Software Technology (AMAST2010), 23-25 June 2010, Manoir St-Castin Quebec, Canada. Lecture Notes in Computer Science, 6486, pp. 111-127, 2011.
  64. Ekaterina Komendantskaya, Krysia Broda and Artur d'Avila Garcez. Using Inductive Types for Ensuring Correctness of Neuro-Symbolic Computations. Proceedings of CiE'2010 - Computability in Europe 2010 - Programs, Proofs, Processes. Ponta Delgada, Portugal, 30 June - 4 July 2010.
  65. E.Komendantskaya. Unification Neural Networks: Unification by Error-Correction Learning. Logic Journal of the IGPL (Oxford Journals) 19(6): 821-847 (2011)
    66. 2009
  66. E.Komendantskaya. Neurons OR Symbols: Why Does OR Remain Exclusive? Position paper. Proceedings of the International Conference on Neural Computation (ICNC), 2009.
  67. E.Komendantskaya. Parallel Rewriting in Neural Networks. Proceedings of the International Conference on Neural Computation (ICNC), 2009.
  68. Y.Bertot and E.Komendantskaya. Using Structural Recursion for Corecursion TYPES'08 LNCS 5497, Springer, 2009; pages 220-236.
  69. E.Komendantskaya. Intermediate three -valued regular logics of Kleene(In Russian) Logic Studies, 15: 116-128. 2009. Editor: A.S.Karpenko. Moscow.
    70. 2008, Postdoctoral Year in INRIA, France
  70. E.Komendantskaya and J.Power. Fibrational Semantics for Many-Valued Logic Programs: Grounds for Non-Groundness. Proceedings of JELIA'08, 28 September - 1 October 2008, Dresden, Germany. LNCS 5293, pages 258-271.
  71. E.Komendantskaya. Unification by Error-Correction, Proceedings of NeSy'08 workshop at ECAI'08, 21-25 July 2008, Patras, Greece. CEUR Workshop Proceedings, Vol. 366, 2008. ISSN 1613-0073.
  72. Y. Bertot and E. Komendantskaya. Inductive and Coinductive Components of Corecursive Functions in Coq, Proceedings of CMCS'08, the 9th International Workshop on Coalgebraic Methods in Computer Science, Budapest, Hungary, April 4 - April 6, 2008. ENTCS 203/5 pp.25--47, 2008.
    73. 2007, Year-3 of PhD
  73. E Komendantskaya. A Sequent Calculus for Bilattice-Based Logics and its Many-Sorted Representation. In Automated Reasoning with Analytic TABLEAUX and Related Methods, N.Olivetti, ed.; Proceedings of the 16th International Conference TABLEAUX'2007, Aix en Provence, France, 3-6 July, 2007; LNAI 4548, Springer, pages 165-182.
  74. E. Komendantskaya, M. Lane and A. Seda. Connectionist Representation of Multi-Valued Logic Programs, 2007. In Perspectives of Neural-Symbolic Integration, Barbara Hammer and Pascal Hizler, eds, in Springer Series Computational Intelligence, editor-in-chief Janusz Kacprzyk; pages 259-289.
  75. E. Komendantskaya. First-order Deduction in Neural Networks, In pre-Proceedings of LATA'07, the 1st Conference on Language and Automata Theory and Applications, March 29--April 4, 2007, Tarragona, Spain; pages 307-318.
    76. 2006, Year-2 of PhD
  76. E. Komendantskaya and A. K. Seda. Sound and Complete SLD-resolution for Bilattice-Based Annotated Logic Programs. Electr. Notes Theor. Comput. Sci. 225: 141-159 (2009). Postproceedings volume of the 4th Irish Conf. on Mathematical Foundations of Computer Science and Information Technology (MFCSIT'06), Cork, Ireland, August 1-5, 2006.
  77. E. Komendantskaya and A. K. Seda. Logic Programs with Uncertainty: Neural Computations and Automated Reasoning. In Logical Approaches to Computational Barriers, Proc. of the 2nd Conference on Computability in Europe, A. Beckmann, U. Berger, B. Lowe, J.V.Tucker, eds., CiE 2006, Swansea, UK, June/July 2006; pp. 170-182.
  78. E. Komendantskaya and V. Komendantsky. On Uniform Proof-Theoretical Operational Semantics for Logic Programming. In Perspectives on Universal Logic, J.-Y. Beziau and A.~Costa-Leite, editors, Post-Proceedings volume of the 1st World Congress on Universal Logic (UNILOG-05), 26 March -- 3 April, 2005, Montreux, Switzerland, 2006. Publisher: Polimetrica, Monza, Italy. 16~pages. In print. Available as a BCRI pre-print.
  79. E. Komendantskaya. Many-Sorted Semantics for Many-Valued Annotated Logic Programs. Proc. 4th Irish Conf. Mathematical Foundations of Computer Science and Information Technology (MFCSIT'06), Cork, Ireland, August 1-5, 2006, pp. 225--229.
  80. E. Komendantskaya and A.Seda. Operational Semantics for Bilattice-Based Annotated Logic Programs. Proc. 4th Irish Conf. Mathematical Foundations of Computer Science and Information Technology (MFCSIT'06), Cork, Ireland, August 1-5, 2006, pp. 229--233.
    81. 2005, Year-1 of PhD
  81. E. Komendantskaya, A. K. Seda, and V. Komendantsky. On Approximation of the Semantic Operators Determined by Bilattice-Based Logic Programs. In Proc. 7th International Workshop on First-Order Theorem Proving (FTP'05), pages 112--130, Koblenz, Germany, September 15--17, 2005.
  82. E. Komendantskaya and V. Komendantsky. Uniform Operational Semantics of Logic Programming and Sequent Calculus. Proceedings of the 1st World Congress on Universal Logic (UNILOG-05), 26 March -- 3 April, 2005, Montreux, Switzerland, 2006. pp.73--74.
    83. Prior to PhD
  83. E. Komendantskaya. Non-Commutative Many-Valued Functions. Proceedings of the XI International Conference for Undergraduate and Graduate Students and Young Scientists "Lomonosov", 12--15 April 2004, Moscow, Russia; pp. 419--421.
  84. E. Komendantskaya. Kleene Regular Intermediate Three-Valued Logics. Proceedings of Smirnov Readings, 4th Interantional Conference. IPhRAS, 2003, p.80--82.