SICSA
The Annual SICSA Conference
ek19, www.macs.hw.ac.uk/~ek19/
Saturday, 26st September 2020 @09:32:00
I am giving a talk AI Verification, in Need of Programming Language Support at the SICSA Conference
Read More »
LAIV
LAIV: Lab for AI and Verification
ek19, www.macs.hw.ac.uk/~ek19/
Monday, 27st April 2020 @16:15:00
LAIV -- the Lab for AI and Verification continues its weekly seminars on-line and has recently announced several PhD and postdoctoral vacancies .
Read More »
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.