New PhD student
th May 2017 @08:15:00
A new PhD student -- Alasdair Hill -- is joining DSG group in Septembr 2017 to work with me on Automated Theorem Proving for Types and Programming Languages.
New Seminar Series on Logic and Programming languages
th March 2017 @11:15:00
Logic and Programming Languages Seminars at MACS are now on the way, every Wednesday at 13.15. A dedicated webpage is
Read More »
My recent and upcoming events:
Invited talk at
Programming Languages and Compilers, 3-5 April 2017. Invited talk at
Algebra and Coalgebra meet Proof Theory , 10-12 April 2017. My PhD student
Yue Li gave a talk about our joint work on Productive Corecursion at Scottish Theorem Proving Workshop, 19 May 2017.
Invited participant at IFIP Working Group 2.8 on Functional Programming, Edinburgh, 11-16 June 2017.
Invited talk at the
Computer-Aided Mathematical Proof workshop, Isaac Newton Institute for Mathematical Sciences,
Cambridge, 10-14 July 2017. I am presenting a paper ``Proof-Mining with Dependent Types" at
CICM'17 in Edinburgh, 17-21 July 2017, Edinburgh.
I am judging
ICFP'17 Student Competition , Oxford, September 2017. PC member in
Haskell Symposium at ICFP'17.
Invited talk at the Shonan meeting ``Enhanced Coinduction", Shonan, Japan, 13-17 November 2017.
My selected publications (full list is given
E.Komendantskaya and J.Heras
Proof Mining with Dependent Types, CICM'17 in Edinburgh, 17-21 July 2017, Edinburgh.
P.Fu and E.Komendantskaya.
Operational Semantics of Resolution and Productivity in Horn Clause Logic. Journal ``Formal Aspect of Computing", 165: 1-22, 2016. 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, 15th-19th December 2013.
Springer LNCS 8312, pp. 389-406, 2013.
Y. Bertot and E. Komendantskaya.
Inductive and Coinductive Components of Corecursive
Functions in Coq,
the 9th International Workshop on Coalgebraic Methods in Computer Science,
Budapest, Hungary, April 4 - April 6, 2008.
ENTCS 203/5 pp.25--47, 2008.