References

  1. Henning Basold, Ekaterina Komendantskaya & Yue Li (2019): Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses. Lecture Notes in Computer Science, pp. 783–813, doi:10.1007/978-3-030-17184-1_28.
  2. Nikolaj Bjørner, Arie Gurfinkel, Kenneth McMillan & Andrey Rybalchenko (2015): Horn clause solvers for program verification. In: Fields of Logic and Computation II. Springer, pp. 24–51, doi:10.1007/978-3-319-23534-9_2. Available at https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-yurifest.pdf.
  3. Nikolaj Bjørner, Kenneth McMillan & Andrey Rybalchenko (2012): Program Verification as Satisfiability Modulo Theories. In: Pascal Fontaine & Amit Goel: SMT 2012. 10th International Workshop on Satisfiability Modulo Theories, EPiC Series in Computing 20. EasyChair, pp. 3–11, doi:10.29007/1l7f.
  4. Julian Bradfield & Colin Stirling (2001): CHAPTER 4 - Modal Logics and mu-Calculi: An Introduction. In: J.A. Bergstra, A. Ponse & S.A. Smolka: Handbook of Process Algebra. Elsevier Science, Amsterdam, pp. 293–330, doi:10.1016/B978-044482830-9/50022-9. Available at http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.9.5944.
  5. Christopher H. Broadbent, Arnaud Carayol, C.-H. Luke Ong & Olivier Serre (2010): Recursion Schemes and Logical Reflection. In: Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11-14 July 2010, Edinburgh, United Kingdom. IEEE Computer Society, pp. 120–129, doi:10.1109/LICS.2010.40. Available at https://hal.archives-ouvertes.fr/hal-00479818.
  6. Toby Cathcart Burn, C.-H. Luke Ong & Steven J. Ramsay (2017): Higher-order Constrained Horn Clauses for Verification. Proc. ACM Program. Lang. 2(POPL), pp. 11:1–11:28, doi:10.1145/3158099.
  7. Pierre Clairambault & Andrzej S. Murawski (2013): Böhm Trees as Higher-Order Recursive Schemes. In: Anil Seth & Nisheeth K. Vishnoi: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013), Leibniz International Proceedings in Informatics (LIPIcs) 24. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany, pp. 91–102, doi:10.4230/LIPIcs.FSTTCS.2013.91.
  8. Alain Colmerauer & Thi-Bich-Hanh Dao (2003): Expressiveness of Full First-Order Constraints in the Algebra of Finite or Infinite Trees. Constraints 8(3), pp. 283–302, doi:10.1023/A:1025675127871. Available at https://hal.archives-ouvertes.fr/hal-00144924.
  9. Bruno Courcelle (1978): A Representation of Trees by Languages I. Theor. Comput. Sci. 6, pp. 255–279, doi:10.1016/0304-3975(78)90008-7. Available at https://core.ac.uk/download/pdf/82601565.pdf.
  10. Khalil Djelloul, Thi-Bich-Hanh Dao & Thom Frühwirth (2008): Theory of finite or infinite trees revisited. Theory Pract. Log. Program. 8(04), pp. 431–489, doi:10.1017/S1471068407003171. Available at https://arxiv.org/abs/0706.4323.
  11. Gopal Gupta, Ajay Bansal, Richard Min, Luke Simon & Ajay Mallya (2007): Coinductive Logic Programming and Its Applications. In: Log. Program.. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 27–44, doi:10.1007/978-3-540-74610-2_4. Available at https://personal.utdallas.edu/~gupta/iclp07paper.pdf.
  12. Joxan Jaffar & Peter J. Stuckey (1986): Semantics of infinite tree logic programming. Theor. Comput. Sci. 46, pp. 141–158, doi:10.1016/0304-3975(86)90027-7.
  13. Petr Jancar (2012): Decidability of DPDA Language Equivalence via First-Order Grammars. In: Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012, pp. 415–424, doi:10.1109/LICS.2012.51. Available at https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.1080.2859&rep=rep1&type=pdf.
  14. Naoki Kobayashi, Étienne Lozes & Florian Bruse (2017): On the Relationship between Higher-Order Recursion Schemes and Higher-Order Fixpoint Logic. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017. Association for Computing Machinery, New York, NY, USA, pp. 246–259, doi:10.1145/3009837.3009854.
  15. Naoki Kobayashi & C.-H. Luke Ong (2009): A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes. In: Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, 11-14 August 2009, Los Angeles, CA, USA. IEEE Computer Society, pp. 179–188, doi:10.1109/LICS.2009.29. Available at https://www-kb.is.s.u-tokyo.ac.jp/~koba/papers/hors-type.pdf.
  16. Naoki Kobayashi, Takeshi Tsukada & Keiichi Watanabe (2018): Higher-Order Program Verification via HFL Model Checking. In: Amal Ahmed: Programming Languages and Systems. Springer International Publishing, Cham, pp. 711–738, doi:10.1007/978-3-319-89884-1_25. Available at https://arxiv.org/abs/1710.08614.
  17. Ekaterina Komendantskaya & Yue Li (2017): Productive corecursion in logic programming. Theory and Practice of Logic Programming 17(5-6), pp. 906–923, doi:10.1017/S147106841700028X. Available at http://arxiv.org/abs/1707.01541.
  18. Ekaterina Komendantskaya & Yue Li (2018): Towards Coinductive Theory Exploration in Horn Clause Logic: Position Paper. In: Temesghen Kahsai & German Vidal: Proceedings 5th Workshop on Horn Clauses for Verification and Synthesis, Oxford, UK, 13th July 2018, Electronic Proceedings in Theoretical Computer Science 278. Open Publishing Association, pp. 27–33, doi:10.4204/EPTCS.278.5.
  19. Ekaterina Komendantskaya, John Power & Martin Schmidt (2016): Coalgebraic logic programming: from Semantics to Implementation. Journal of Logic and Computation 26(2), pp. 745–783, doi:10.1093/logcom/exu026. Available at https://arxiv.org/abs/1312.6568.
  20. Michael J. Maher (1988): Complete axiomatizations of the algebras of finite, rational and infinite trees. In: LICS, pp. 348–357, doi:10.1109/LICS.1988.5132. Available at https://www.computer.org/csdl/pds/api/csdl/proceedings/download-article/12OmNyLiuB4/pdf.
  21. C.-H. Luke Ong (2006): On Model-Checking Trees Generated by Higher-Order Recursion Schemes. In: 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings, pp. 81–90, doi:10.1109/LICS.2006.38. Available at https://www.cs.ox.ac.uk/people/luke.ong/personal/publications/lics06.pdf.
  22. C.-H. Luke Ong (2015): Higher-Order Model Checking: An Overview. In: 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pp. 1–15, doi:10.1109/LICS.2015.9. Available at http://www.cs.ox.ac.uk/people/luke.ong/personal/publications/LICS15.pdf.
  23. C.-H. Luke Ong & Dominik Wagner (2019): HoCHC: A Refutationally Complete and Semantically Invariant System of Higher-order Logic Modulo Theories. In: 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pp. 1–14, doi:10.1109/LICS.2019.8785784. Available at https://arxiv.org/abs/1902.10396.
  24. Long Pham, Steven J. Ramsay & C.-H. Luke Ong (2018): Defunctionalization of Higher-Order Constrained Horn Clauses. CoRR abs/1810.03598. Available at http://arxiv.org/abs/1810.03598.
  25. Sylvain Salvati & Igor Walukiewicz (2014): Krivine machines and higher-order schemes. Information and Computation 239, pp. 340–355, doi:10.1016/j.ic.2014.07.012. Available at https://hal.inria.fr/inria-00589407/document.
  26. Géraud Sénizergues (2001): L(A)=L(B)? decidability results from complete formal systems. Theor. Comput. Sci. 251(1-2), pp. 1–166, doi:10.1016/S0304-3975(00)00285-1.
  27. Géraud Sénizergues (2002): L(A)=L(B)? A simplified decidability proof. Theor. Comput. Sci. 281(1-2), pp. 555–608, doi:10.1016/S0304-3975(02)00027-0.
  28. Luke Simon, Ajay Bansal, Ajay Mallya & Gopal Gupta (2007): Co-Logic Programming: Extending Logic Programming with Coinduction. In: Autom. Lang. Program.. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 472–483, doi:10.1007/978-3-540-73420-8_42.
  29. Rick Statman (2004): On the Lambda-Y calculus. Annals of Pure and Applied Logic 130(1-3 SPEC. ISS.), pp. 325–337, doi:10.1016/j.apal.2004.04.004. Available at https://core.ac.uk/download/pdf/82358399.pdf.
  30. Colin Stirling (2001): Decidability of DPDA equivalence. Theor. Comput. Sci. 255(1-2), pp. 1–31, doi:10.1016/S0304-3975(00)00389-3. Available at http://homepages.inf.ed.ac.uk/cps/dpda.pdf.
  31. Mahesh Viswanathan & Ramesh Viswanathan (2004): A Higher Order Modal Fixed Point Logic. In: Philippa Gardner & Nobuko Yoshida: CONCUR 2004 - Concurrency Theory. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 512–528, doi:10.1007/978-3-540-28644-8_33. Available at http://vmahesh.cs.illinois.edu/papers/concur04.pdf.
  32. Dominik Wagner (2019). private communication.
  33. Igor Walukiewicz (2016): Automata Theory and Higher-Order Model-Checking. ACM SIGLOG News 3(4), pp. 13–31, doi:10.1145/3026744.3026745. Available at https://www.labri.fr/perso/igw/Papers/igw-siglog16.pdf.
  34. Fabian Zaiser & C.-H. Luke Ong (2020): The Extended Theory of Trees and Algebraic (Co)datatypes. Electronic Proceedings in Theoretical Computer Science 320, pp. 167–196, doi:10.4204/eptcs.320.14.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org