Modeling Infinite Behaviour by Corules

Authors Davide Ancona , Francesco Dagnino , Elena Zucca



PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2018.21.pdf
  • Filesize: 0.76 MB
  • 31 pages

Document Identifiers

Author Details

Davide Ancona
  • DIBRIS, University of Genova, Italy
Francesco Dagnino
  • DIBRIS, University of Genova, Italy
Elena Zucca
  • DIBRIS, University of Genova, Italy

Cite AsGet BibTex

Davide Ancona, Francesco Dagnino, and Elena Zucca. Modeling Infinite Behaviour by Corules. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 21:1-21:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.ECOOP.2018.21

Abstract

Generalized inference systems have been recently introduced, and used, among other applications, to define semantic judgments which uniformly model terminating computations and divergence. We show that the approach can be successfully extended to more sophisticated notions of infinite behaviour, that is, to express that a diverging computation produces some possibly infinite result. This also provides a motivation to smoothly extend the theory of generalized inference systems to include, besides coaxioms, also corules, a more general notion for which significant examples were missing until now. We first illustrate the approach on a lambda-calculus with output effects, for which we also provide an alternative semantics based on standard notions, and a complete proof of the equivalence of the two semantics. Then, we consider a more involved example, that is, an imperative Java-like language with I/O primitives.

Subject Classification

ACM Subject Classification
  • Theory of computation → Operational semantics
Keywords
  • Operational semantics
  • coinduction
  • trace semantics

Metrics

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

References

  1. Peter Aczel. An introduction to inductive definitions. In Jon Barwise, editor, Handbook of Mathematical logic, pages 739-782. North Holland, 1977. Google Scholar
  2. Nada Amin and Tiark Rompf. Type soundness proofs with definitional interpreters. In Giuseppe Castagna and Andrew D. Gordon, editors, ACM Symp. on Principles of Programming Languages 2017, pages 666-679. ACM Press, 2017. URL: http://dx.doi.org/10.1145/3009837.
  3. Davide Ancona. Soundness of object-oriented languages with coinductive big-step semantics. In James Noble, editor, ECOOP'12 - Object-Oriented Programming, volume 7313 of Lecture Notes in Computer Science, pages 459-483. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-31057-7_21.
  4. Davide Ancona. How to prove type soundness of Java-like languages without forgoing big-step semantics. In David J. Pearce, editor, FTfJP'14 - Formal Techniques for Java-like Programs, pages 1:1-1:6. ACM Press, 2014. URL: http://dx.doi.org/10.1145/2635631.2635846.
  5. Davide Ancona, Francesco Dagnino, and Elena Zucca. Generalizing inference systems by coaxioms. In Hongseok Yang, editor, ESOP 2017 - European Symposium on Programming, volume 10201 of Lecture Notes in Computer Science, pages 29-55. Springer, 2017. URL: http://dx.doi.org/10.1007/978-3-662-54434-1_2.
  6. Davide Ancona, Francesco Dagnino, and Elena Zucca. Reasoning on divergent computations with coaxioms. PACMPL, 1(OOPSLA):81:1-81:26, 2017. URL: http://dx.doi.org/10.1145/3133905.
  7. Arthur Charguéraud. Pretty-big-step semantics. In Matthias Felleisen and Philippa Gardner, editors, ESOP 2013 - European Symposium on Programming, volume 7792 of Lecture Notes in Computer Science, pages 41-60. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-37036-6_3.
  8. Patrick Cousot and Radhia Cousot. Inductive definitions, semantics and abstract interpretations. In Ravi Sethi, editor, ACM Symp. on Principles of Programming Languages 1992, pages 83-94. ACM Press, 1992. URL: http://dx.doi.org/10.1145/143165.143184.
  9. Patrick Cousot and Radhia Cousot. Bi-inductive structural semantics. Information and Computation, 207(2):258-283, 2009. URL: http://dx.doi.org/10.1016/j.ic.2008.03.025.
  10. Nils Anders Danielsson. Total parser combinators. In Intl. Conf. on Functional Programming 2010, pages 285-296. ACM Press, 2010. Google Scholar
  11. Nils Anders Danielsson. Operational semantics using the partiality monad. In Peter Thiemann and Robby Bruce Findler, editors, Intl. Conf. on Functional Programming 2012, pages 127-138. ACM Press, 2012. URL: http://dx.doi.org/10.1145/2364527.2364546.
  12. Bart Jacobs. Introduction to Coalgebra: Towards Mathematics of States and Observation, volume 59 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. URL: http://dx.doi.org/10.1017/CBO9781316823187.
  13. Xavier Leroy and Hervé Grall. Coinductive big-step operational semantics. Information and Computation, 207(2):284-304, 2009. URL: http://dx.doi.org/10.1016/j.ic.2007.12.004.
  14. Keiko Nakata and Tarmo Uustalu. Trace-based coinductive operational semantics for while. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics - TPHOLs 2009, volume 5674 of Lecture Notes in Computer Science, pages 375-390. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-03359-9_26.
  15. Keiko Nakata and Tarmo Uustalu. A Hoare logic for the coinductive trace-based big-step semantics of while. In Andrew D. Gordon, editor, ESOP 2010 - European Symposium on Programming, volume 6012 of Lecture Notes in Computer Science, pages 488-506. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-11957-6_26.
  16. Keiko Nakata and Tarmo Uustalu. Resumptions, weak bisimilarity and big-step semantics for while with interactive I/O: an exercise in mixed induction-coinduction. In Luca Aceto and Pawel Sobocinski, editors, SOS'10 - Structural Operational Semantics, volume 32 of Electronic Proceedings in Theoretical Computer Science, pages 57-75, 2010. URL: http://dx.doi.org/10.4204/EPTCS.32.5.
  17. Scott Owens, Magnus O. Myreen, Ramana Kumar, and Yong Kiam Tan. Functional big-step semantics. In Peter Thiemann, editor, ESOP 2016 - European Symposium on Programming, volume 9632 of Lecture Notes in Computer Science, pages 589-615. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-662-49498-1_23.
  18. C. B. Poulsen and P. D. Mosses. Flag-based big-step semantics. Journal of Logical and Algebraic Methods in Programming, 2016. Google Scholar
  19. John C. Reynolds. Definitional interpreters for higher-order programming languages. In ACM ’72, Proceedings of the ACM annual conference, volume 2, pages 717–-740. ACM Press, 1972. Google Scholar
  20. Jan J. M. M. Rutten. Universal coalgebra: a theory of systems. Theoretical Computer Science, 249(1):3-80, 2000. URL: http://dx.doi.org/10.1016/S0304-3975(00)00056-6.
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