@book(Book:95:Abiteboul:DBFundamentals,
 author       = {S. Abiteboul and R. Hull and V. Vianu},
 year         = {1995},
 title        = {Foundations of Databases},
 publisher    = {Addison-Wesley},
)
@inproceedings(DBLP:conf/lpar/AxelssonL07,
 author       = {R. Axelsson and M. Lange},
 year         = {2007},
 title        = {Model Checking the First-Order Fragment of Higher-Order Fixpoint Logic},
 booktitle    = {Proc.\ 14th Int.\ Conf.\ on Logic for Programming, Artificial Intelligence, and Reasoning, {LPAR'07}},
 series       = {LNCS},
 volume       = {4790},
 publisher    = {Springer},
 pages        = {62--76},
 doi          = {10.1007/978-3-540-75560-9_7},
)
@inproceedings(la-reachpdl:2011,
 author       = {R. Axelsson and M. Lange},
 year         = {2011},
 title        = {Formal Language Constrained Reachability and Model Checking Propositional Dynamic Logics},
 booktitle    = {Proc.\ 5th Workshop on Reachability Problems, {RP'11}},
 series       = {LNCS},
 volume       = {6945},
 publisher    = {Springer},
 pages        = {45--57},
 doi          = {10.1007/978-3-642-24288-5\_6},
)
@article(als-mchfl07,
 author       = {R. Axelsson and M. Lange and R. Somla},
 year         = {2007},
 title        = {The Complexity of Model Checking Higher-Order Fixpoint Logic},
 journal      = {Logical Methods in Computer Science},
 volume       = {3},
 pages        = {1--33},
 doi          = {10.2168/LMCS-3(2:7)2007},
)
@book(books/daglib/0020348,
 author       = {C. Baier and J.-P. Katoen},
 year         = {2008},
 title        = {Principles of model checking},
 publisher    = {MIT Press},
)
@article(journals/tods/BarceloLLW12,
 author       = {P. Barcel{\'o} and L. Libkin and A. W. Lin and P. T. Wood},
 year         = {2012},
 title        = {Expressive Languages for Path Queries over Graph-Structured Data},
 journal      = {ACM Trans. Database Syst},
 volume       = {37},
 number       = {4},
 pages        = {31:1--31:46},
 doi          = {10.1145/2389241.2389250},
)
@article(Barrett:2000:FLC,
 author       = {C. Barrett and R. Jacob and M. Marathe},
 year         = {2000},
 title        = {Formal-Language-Constrained Path Problems},
 journal      = {SIAM Journal on Computing},
 volume       = {30},
 number       = {3},
 pages        = {809--837},
 doi          = {10.1137/S0097539798337716},
)
@inproceedings(Bhat:1996:ELM,
 author       = {G. Bhat and R. Cleaveland},
 year         = {1996},
 title        = {Efficient Local Model-Checking for Fragments of the Modal $\mu$-Calculus},
 booktitle    = {Proc. 2nd Int. Workshop on Tools and Algorithms for Construction and Analysis of Systems, {TACAS'96}},
 series       = {LNCS},
 volume       = {1055},
 publisher    = {Springer},
 pages        = {107--126},
 doi          = {10.1109/LICS.1996.561358},
)
@inproceedings(DBLP:conf/csl/BroadbentK13,
 author       = {C. H. Broadbent and N. Kobayashi},
 year         = {2013},
 title        = {Saturation-Based Model Checking of Higher-Order Recursion Schemes},
 editor       = {S. Ronchi Della Rocca},
 booktitle    = {Computer Science Logic 2013 {(CSL} 2013), {CSL} 2013, September 2-5, 2013, Torino, Italy},
 series       = {LIPIcs},
 volume       = {23},
 publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
 pages        = {129--148},
 doi          = {10.4230/LIPIcs.CSL.2013.129},
)
@inproceedings(BLL:RP17,
 author       = {F. Bruse and M. Lange and {\'{E}}. Lozes},
 year         = {2017},
 title        = {Space-Efficient Fragments of Higher-Order Fixpoint Logic},
 booktitle    = {Proc.\ 11th Workshop on Reachability Problems, {RP'17}},
 series       = {LNCS},
 volume       = {10506},
 publisher    = {Springer},
 pages        = {26--41},
 doi          = {10.1007/978-3-319-67089-8_3},
)
@article(burn1986strictness,
 author       = {G. L. Burn and C. Hankin and S. Abramsky},
 year         = {1986},
 title        = {Strictness analysis for higher-order functions},
 journal      = {Science of computer programming},
 volume       = {7},
 pages        = {249--278},
 doi          = {10.1016/0167-6423(86)90010-9},
)
@inproceedings(le1993groundness,
 author       = {B. Le Charlier and P. Van Hentenryck},
 year         = {1993},
 title        = {Groundness analysis for {P}rolog: implementation and evaluation of domain prop},
 booktitle    = {Proc.\ ACM SIGPLAN Symp.\ on Partial Evaluation and Semantics-Based Program Manipulation, {PEPM'93}},
 pages        = {99--110},
 doi          = {10.1145/154630.154641},
)
@inproceedings(cousot1977abstract,
 author       = {P. Cousot and R. Cousot},
 year         = {1977},
 title        = {Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints},
 booktitle    = {Proc.\ 4th ACM SIGACT-SIGPLAN Symp.\ on Principles of Programming Languages, {POPL'77}},
 pages        = {238--252},
 doi          = {10.1145/512950.512973},
)
@inproceedings(cousot1994higher,
 author       = {P. Cousot and R. Cousot},
 year         = {1994},
 title        = {Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages)},
 booktitle    = {Proc.\ Int.\ Conf.\ on Computer Languages, {ICCL'94}},
 organization = {IEEE},
 pages        = {95--112},
 doi          = {10.1109/ICCL.1994.288389},
)
@book(TLCS-DGL16,
 author       = {S. Demri and V. Goranko and M. Lange},
 year         = {2016},
 title        = {Temporal Logics in Computer Science},
 series       = {Cambridge Tracts in Theoretical Computer Science},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9781139236119},
)
@inproceedings(distefano2006local,
 author       = {D. Distefano and P. W. O'Hearn and H. Yang},
 year         = {2006},
 title        = {A local shape analysis based on separation logic},
 booktitle    = {Proc.\ 12th Int.\ Conf.\ on Tools and Algorithms for the Construction and Analysis of Systems, {TACAS'06}},
 organization = {Springer},
 pages        = {287--302},
 doi          = {10.1007/11691372\_19},
)
@inproceedings(ICALP::EmersonC1980,
 author       = {E. A. Emerson and E. M. Clarke},
 year         = {1980},
 title        = {Characterizing Correctness Properties of Parallel Programs Using Fixpoints},
 editor       = {J. W. de Bakker and J. van Leeuwen},
 booktitle    = {Proc. 7th Int. Coll.\ on Automata, Languages and Programming, {ICALP'80}},
 series       = {LNCS},
 volume       = {85},
 publisher    = {Springer},
 pages        = {169--181},
 doi          = {10.1007/3-540-10003-2\_69},
)
@inproceedings(fecht1996even,
 author       = {C. Fecht and H. Seidl},
 year         = {1996},
 title        = {An even faster solver for general systems of equations},
 booktitle    = {Proc.\ 3rd Int.\ Static Analysis Symp., {SAS'96}},
 organization = {Springer},
 pages        = {189--204},
 doi          = {10.1007/3-540-61739-6\_42},
)
@book(IB-C992509,
 author       = {N. Immerman},
 year         = {1999},
 title        = {Descriptive complexity},
 series       = {Graduate texts in computer science},
 publisher    = {Springer},
 doi          = {10.1007/978-1-4612-0539-5},
)
@inproceedings(Jorgenson94,
 author       = {J{\o}rgensen, N.},
 year         = {1994},
 title        = {Finding Fixpoints in Finite Function Spaces using Neededness Analysis and Chaotic Iteration},
 booktitle    = {Proc.\ 1st Int.\ Static Analysis Symposium, {SAS'94}},
 series       = {LNCS},
 volume       = {864},
 publisher    = {Springer},
 pages        = {329--345},
 doi          = {10.1007/3-540-58485-4_50},
)
@article(Kleene:1938,
 author       = {S. C. Kleene},
 year         = {1938},
 title        = {On Notation for Ordinal Numbers},
 journal      = {Journal Symbolic Logic},
 volume       = {3},
 number       = {4},
 pages        = {150--155},
 doi          = {10.2307/2267778},
)
@inproceedings(DBLP:conf/popl/KobayashiLB17,
 author       = {N. Kobayashi and {\'{E}}. Lozes and F. Bruse},
 year         = {2017},
 title        = {On the relationship between higher-order recursion schemes and higher-order fixpoint logic},
 booktitle    = {Proc.\ 44th {ACM} {SIGPLAN} Symp.\ on Principles of Programming Languages, {POPL'17}},
 publisher    = {{ACM}},
 pages        = {246--259},
 doi          = {10.1145/3093333.3009854},
)
@article(Kozen83,
 author       = {D. Kozen},
 year         = {1983},
 title        = {Results on the Propositional $\mu$-calculus},
 journal      = {TCS},
 volume       = {27},
 pages        = {333--354},
 doi          = {10.1016/0304-3975(82)90125-6},
)
@inproceedings(conf/fct/LangeL15,
 author       = {M. Lange and {\'{E}}. Lozes},
 year         = {2015},
 title        = {Conjunctive Visibly-Pushdown Path Queries},
 booktitle    = {Proc.\ 20th Int.\ Symp.\ on Fundamentals of Computation Theory, {FCT'15}},
 series       = {LNCS},
 volume       = {9210},
 publisher    = {Springer},
 pages        = {327--338},
 doi          = {10.1007/978-3-319-22177-9\_25},
)
@inproceedings(lev2000tvla,
 author       = {Lev-Ami, T. and M. Sagiv},
 year         = {2000},
 title        = {TVLA: A system for implementing static analyses},
 booktitle    = {Proc.\ 7th Int.\ Static Analysis Symp., {SAS'00}},
 organization = {Springer},
 pages        = {280--301},
 doi          = {10.1007/978-3-540-45099-3\_15},
)
@article(Maslov74,
 author       = {A. N. Maslov},
 year         = {1974},
 title        = {The hierarchy of indexed languages of an arbitrary level},
 journal      = {Dokl. Akad. Nauk SSSR},
 volume       = {217},
 pages        = {1013--1016},
)
@inproceedings(mycroft1980theory,
 author       = {A. Mycroft},
 year         = {1980},
 title        = {The theory and practice of transforming call-by-need into call-by-value},
 booktitle    = {Proc.\ 4th Int.\ Symp.\ on Programming},
 organization = {Springer},
 pages        = {269--281},
 doi          = {10.1007/3-540-09981-6\_19},
)
@book(nielson2015principles,
 author       = {F. Nielson and H. R. Nielson and C. Hankin},
 year         = {1999},
 title        = {Principles of program analysis},
 publisher    = {Springer},
 doi          = {10.1007/978-3-662-03811-6},
)
@inproceedings(conf/lics/Ong06,
 author       = {C.-H. L. Ong},
 year         = {2006},
 title        = {On Model-Checking Trees Generated by Higher-Order Recursion Schemes},
 booktitle    = {Proc.\ 21st IEEE Symp. on Logic in Computer Science, {LICS'06}},
 publisher    = {IEEE Computer Society},
 pages        = {81--90},
 doi          = {10.1109/LICS.2006.38},
)
@inproceedings(DBLP:conf/popl/RamsayNO14,
 author       = {S. J. Ramsay and R. P. Neatherway and C.{-}H. Luke Ong},
 year         = {2014},
 title        = {A type-directed abstraction refinement approach to higher-order model checking},
 booktitle    = {Proc.\ 41st Ann.\ {ACM} {SIGPLAN-SIGACT} Symp.\ on Principles of Programming Languages, {POPL'14}},
 publisher    = {{ACM}},
 pages        = {61--72},
 doi          = {10.1145/2535838.2535873},
)
@book(SimoTenn99,
 author       = {D. Simovici and R. L. Tenney},
 year         = {1999},
 title        = {Theory of Formal Languages with Applications},
 publisher    = {World Scientific},
 doi          = {10.1142/3991},
)
@article(Tars55,
 author       = {A. Tarski},
 year         = {1955},
 title        = {A Lattice-theoretical Fixpoint Theorem and its Application},
 journal      = {Pacific Journal of Mathematics},
 volume       = {5},
 pages        = {285--309},
 doi          = {10.2140/pjm.1955.5.285},
)
@inproceedings(DBLP:conf/concur/ViswanathanV04,
 author       = {M. Viswanathan and R. Viswanathan},
 year         = {2004},
 title        = {A Higher Order Modal Fixed Point Logic},
 booktitle    = {Proc.\ 15th Int.\ Conf.\ on Concurrency Theory, {CONCUR'04}},
 series       = {LNCS},
 volume       = {3170},
 publisher    = {Springer},
 pages        = {512--528},
 doi          = {10.1007/978-3-540-28644-8_33},
)
@inproceedings(Wand74,
 author       = {M. Wand},
 year         = {1974},
 title        = {An algebraic formulation of the Chomsky hierarchy},
 editor       = {E. G. Manes},
 booktitle    = {Category Theory Applied to Computation and Control, Proceedings of the First International Symposium, San Francisco, CA, USA, February 25-26, 1974, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {25},
 publisher    = {Springer},
 pages        = {209--213},
 doi          = {10.1007/3-540-07142-3\_84},
)
@book(Winskel93,
 author       = {G. Winskel},
 year         = {1993},
 title        = {The Formal Semantics of Programming Languages: An Introduction.},
 series       = {Foundations of Computing series},
 publisher    = {MIT Press},
 doi          = {10.7551/mitpress/3054.001.0001},
)