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