References

  1. S. Abiteboul, R. Hull & V. Vianu (1995): Foundations of Databases. Addison-Wesley.
  2. 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.
  3. 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.
  4. 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.
  5. C. Baier & J.-P. Katoen (2008): Principles of model checking. MIT Press.
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. 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.
  11. 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.
  12. 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.
  13. 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.
  14. 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.
  15. 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.
  16. 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.
  17. 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.
  18. 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.
  19. N. Immerman (1999): Descriptive complexity. Graduate texts in computer science. Springer, doi:10.1007/978-1-4612-0539-5.
  20. 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.
  21. S. C. Kleene (1938): On Notation for Ordinal Numbers. Journal Symbolic Logic 3(4), pp. 150–155, doi:10.2307/2267778.
  22. 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.
  23. D. Kozen (1983): Results on the Propositional μ-calculus. TCS 27, pp. 333–354, doi:10.1016/0304-3975(82)90125-6.
  24. 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.
  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.
  26. A. N. Maslov (1974): The hierarchy of indexed languages of an arbitrary level. Dokl. Akad. Nauk SSSR 217, pp. 1013–1016.
  27. 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.
  28. F. Nielson, H. R. Nielson & C. Hankin (1999): Principles of program analysis. Springer, doi:10.1007/978-3-662-03811-6.
  29. 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.
  30. 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.
  31. D. Simovici & R. L. Tenney (1999): Theory of Formal Languages with Applications. World Scientific, doi:10.1142/3991.
  32. 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.
  33. 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.
  34. 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.
  35. G. Winskel (1993): The Formal Semantics of Programming Languages: An Introduction.. Foundations of Computing series. MIT Press, doi:10.7551/mitpress/3054.001.0001.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org