A Model for Behavioural Properties of Higher-order Programs

Authors Sylvain Salvati, Igor Walukiewicz



PDF
Thumbnail PDF

File

LIPIcs.CSL.2015.229.pdf
  • Filesize: 1.23 MB
  • 15 pages

Document Identifiers

Author Details

Sylvain Salvati
Igor Walukiewicz

Cite AsGet BibTex

Sylvain Salvati and Igor Walukiewicz. A Model for Behavioural Properties of Higher-order Programs. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 229-243, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.CSL.2015.229

Abstract

We consider simply typed lambda-calculus with fixpoints as a non-interpreted functional programming language: the result of the execution of a program is its normal form that can be seen as a potentially infinite tree of calls to built-in operations. Properties of such trees are properties of executions of programs and monadic second-order logic (MSOL) is well suited to express them. For a given MSOL property we show how to construct a finitary model recognizing it. In other words, the value of a lambda-term in the model determines if the tree that is the result of the execution of the term satisfies the property. The finiteness of the construction has as consequences many known results about the verification of higher-order programs in this framework.
Keywords
  • Simply typed lambda-Y-calculus
  • Monadic second order logic
  • semantic models

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. K. Aehlig. A finite semantics of simply-typed lambda terms for infinite runs of automata. Logical Methods in Computer Science, 3(1):1-23, 2007. Google Scholar
  2. C. Broadbent, A. Carayol, L. Ong, and O. Serre. Recursion schemes and logical reflection. In LICS, pages 120-129, 2010. Google Scholar
  3. C. Broadbent and C.-H. L. Ong. On global model checking trees generated by higher-order recursion schemes. In FOSSACS, volume 5504 of LNCS, pages 107-121, 2009. Google Scholar
  4. C. H. Broadbent, A. Carayol, M. Hague, and O. Serre. C-shore: a collapsible approach to higher-order verification. In ICFP, pages 13-24. ACM, 2013. Google Scholar
  5. Werner Damm. The IO- and OI-hierarchies. Theoretical Computer Science, 20:95-207, 1982. Google Scholar
  6. J. Engelfriet and E. M. Schmidt. IO and OI. I. Journal of computer and system sciences, 15:328-353, 1977. Google Scholar
  7. J. Engelfriet and E. M. Schnidt. IO and OI. II. Journal of computer and system sciences, 16:67-99, 1978. Google Scholar
  8. Charles Grellois and Paul-André Melliès. An infinitary model of linear logic. In FOSSACS 15, volume 9034 of LNCS, pages 41-55, 2015. Google Scholar
  9. A. Haddad. Model checking and functional program transformations. In FSTTCS, volume 24 of LIPIcs, pages 115-126, 2013. Google Scholar
  10. M. Hofmann and W. Chen. Abstract interpretation from büchi automata. In LICS-CSL, pages 51:1-51:10, 2014. Google Scholar
  11. Yu I Ianov. The logical schemes of algorithms. Problems of cybernetics, 1:82-140, 1960. Google Scholar
  12. A Jeffrey. Functional reactive types. In CSL-LICS, pages 54:1-54:10, 2014. Google Scholar
  13. Teodor Knapik, Damian Niwinski, and Pawel Urzyczyn. Higher-order pushdown trees are easy. In FoSSaCS, volume 2303, pages 205-222, 2002. Google Scholar
  14. N. Kobayashi. Model checking higher-order programs. J. ACM, 60(3):20-89, 2013. Google Scholar
  15. N. Kobayashi and L. Ong. A type system equivalent to modal mu-calculus model checking of recursion schemes. In LICS, pages 179-188, 2009. Google Scholar
  16. P.A. Mellies. Linear logic and higher-order model checking, June 2014. http://www.pps.univ-paris-diderot.fr/~mellies/slides/workshop-IHP-model-checking.pdf. Google Scholar
  17. P.A. Mellies. private communication, June 2014. Google Scholar
  18. M. Naik and J. Palsberg. A type system equivalent to a model checker. ACM Trans. Program. Lang. Syst., 30(5), 2008. Google Scholar
  19. C.-H. L. Ong. On model-checking trees generated by higher-order recursion schemes. In LICS, pages 81-90, 2006. Google Scholar
  20. S. J. Ramsay, R. P. Neatherway, and C.-H. L. Ong. A type-directed abstraction refinement approach to higher-order model checking. In POPL, pages 61-72. ACM, 2014. Google Scholar
  21. S. Salvati and I. Walukiewicz. Evaluation is MSOL-compatible. In FSTTCS, volume 24 of LIPIcs, pages 103-114, 2013. Google Scholar
  22. S. Salvati and I. Walukiewicz. Using models to model-check recursive schemes. In TLCA, volume 7941 of LNCS, pages 189-204, 2013. Google Scholar
  23. Sylvain Salvati. Recognizability in the Simply Typed Lambda-Calculus. In WOLIC, volume 5514 of LNCS, pages 48-60, 2009. Google Scholar
  24. Sylvain Salvati and Igor Walukiewicz. A model for behavioural properties of higher-order programs, April 2015. https://hal.archives-ouvertes.fr/hal-01145494. Google Scholar
  25. Sylvain Salvati and Igor Walukiewicz. Typing weak MSOL properties. In FOSSACS 15, volume 9034, pages 343-357, 2015. Google Scholar
  26. K. Terui. Semantic evaluation, intersection types and complexity of simply typed lambda calculus. In RTA, volume 15 of LIPIcs, pages 323-338. Schloss Dagstuhl, 2012. Google Scholar
  27. T. Tsukada and C.-H. L. Ong. Compositional higher-order model checking via ω-regular games over Böhm trees. In LICS-CSL, pages 78:1-78:10, 2014. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail