Document Open Access Logo

Sound Regular Corecursion in coFJ

Authors Davide Ancona , Pietro Barbieri , Francesco Dagnino , Elena Zucca

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2020.1.pdf
  • Filesize: 0.79 MB
  • 28 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Operational semantics
  • Software and its engineering → Recursion
  • Software and its engineering → Semantics
Keywords
  • Operational semantics
  • coinduction
  • programming paradigms
  • regular terms

Metrics

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

Abstract

The aim of the paper is to provide solid foundations for a programming paradigm natively supporting the creation and manipulation of cyclic data structures. To this end, we describe coFJ, a Java-like calculus where objects can be infinite and methods are equipped with a codefinition (an alternative body). We provide an abstract semantics of the calculus based on the framework of inference systems with corules. In coFJ with this semantics, FJ recursive methods on finite objects can be extended to infinite objects as well, and behave as desired by the programmer, by specifying a codefinition. We also describe an operational semantics which can be directly implemented in a programming language, and prove the soundness of such semantics with respect to the abstract one.

Cite As Get BibTex

Davide Ancona, Pietro Barbieri, Francesco Dagnino, and Elena Zucca. Sound Regular Corecursion in coFJ. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 1:1-1:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.ECOOP.2020.1

Author Details

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

Funding

  • Ancona, Davide: Member of GNCS (Gruppo Nazionale per il Calcolo Scientifico), INdAM (Istituto Nazionale di Alta Matematica "F. Severi")

References

  1. P. Aczel. An introduction to inductive definitions. In Handbook of Mathematical logic. North Holland, 1977. Google Scholar
  2. Davide Ancona. Regular corecursion in Prolog. Computer Languages, Systems & Structures, 39(4):142-162, 2013. Google Scholar
  3. Davide Ancona, Francesco Dagnino, and Elena Zucca. Extending coinductive logic programming with co-facts. In Ekaterina Komendantskaya and John Power, editors, First Workshop on Coalgebra, Horn Clause Logic Programming and Types, CoALP-Ty'16, volume 258 of Electronic Proceedings in Theoretical Computer Science, pages 1-18. Open Publishing Association, 2017. URL: https://doi.org/10.4204/EPTCS.258.1.
  4. Davide Ancona, Francesco Dagnino, and Elena Zucca. Generalizing inference systems by coaxioms. In Hongseok Yang, editor, 26th European Symposium on Programming, ESOP 2017, volume 10201 of Lecture Notes in Computer Science, pages 29-55. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54434-1_2.
  5. Davide Ancona, Francesco Dagnino, and Elena Zucca. Reasoning on divergent computations with coaxioms. PACMPL, 1(OOPSLA):81:1-81:26, 2017. Google Scholar
  6. Davide Ancona, Francesco Dagnino, and Elena Zucca. Modeling infinite behaviour by corules. In ECOOP'18 - Object-Oriented Programming, pages 21:1-21:31, 2018. Google Scholar
  7. Davide Ancona and Agostino Dovier. A theoretical perspective of coinductive logic programming. Fundamenta Informaticae, 140(3-4):221-246, 2015. Google Scholar
  8. Davide Ancona and Elena Zucca. Corecursive Featherweight Java. In FTfJP'12 - Formal Techniques for Java-like Programs, pages 3-10. ACM Press, 2012. Google Scholar
  9. Davide Ancona and Elena Zucca. Safe corecursion in coFJ. In FTfJP'13 - Formal Techniques for Java-like Programs, page 2. ACM Press, 2013. Google Scholar
  10. Pietro Barbieri, Francesco Dagnino, Elena Zucca, and Davide Ancona. Corecursive Featherweight Java revisited. In Alessandra Cherubini, Nicoletta Sabadini, and Simone Tini, editors, ICTCS'19 - Italian Conf. on Theoretical Computer Science, volume 2504 of CEUR Workshop Proceedings, pages 158-170. CEUR-WS.org, 2019. URL: http://ceur-ws.org/Vol-2504/paper19.pdf.
  11. Henning Basold, Ekaterina Komendantskaya, and Yue Li. Coinduction in uniform: Foundations for corecursive proof search with Horn clauses. In Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, pages 783-813, 2019. Google Scholar
  12. B. Courcelle. Fundamental properties of infinite trees. Theoretical Computer Science, 25:95-169, 1983. Google Scholar
  13. Francesco Dagnino. Coaxioms: flexible coinductive definitions by inference systems. Logical Methods in Computer Science, 15(1), 2019. URL: https://lmcs.episciences.org/5277.
  14. E.Komendantskaya et al. A productivity checker for logic programming. Post-proc. LOPSTR'16, 2017. URL: http://arxiv.org/abs/1608.04415.
  15. Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweight Java: A minimal core calculus for Java and GJ. In ACM Symp. on Object-Oriented Programming: Systems, Languages and Applications 1999, pages 132-146. ACM Press, 1999. URL: https://doi.org/10.1145/320384.320395.
  16. Jean-Baptiste Jeannin and Dexter Kozen. Computing with capsules. Journal of Automata, Languages and Combinatorics, 17(2-4):185-204, 2012. URL: https://doi.org/10.25596/jalc-2012-185.
  17. Jean-Baptiste Jeannin, Dexter Kozen, and Alexandra Silva. Cocaml: Functional programming with regular coinductive types. Fundamenta Informaticae, 150:347-377, 2017. Google Scholar
  18. E. Komendantskaya et al. Coalgebraic logic programming: from semantics to implementation. J. Logic and Computation, 26(2):745, 2016. URL: https://doi.org/10.1093/logcom/exu026.
  19. X. Leroy and H. Grall. Coinductive big-step operational semantics. Information and Computation, 207(2):284-304, 2009. Google Scholar
  20. L. Simon. Extending logic programming with coinduction. PhD thesis, University of Texas at Dallas, 2006. Google Scholar
  21. L. Simon, A. Bansal, A. Mallya, and G. Gupta. Co-logic programming: Extending logic programming with coinduction. In ICALP 2007, pages 472-483, 2007. 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
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact