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