2026-07-26T03:11:31Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9226 2024-03-06T10:43:40Z ddc:004 open_access

Modeling Infinite Behaviour by Corules Ancona, Davide Dagnino, Francesco Zucca, Elena Operational semantics coinduction trace semantics 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Davide Ancona and Francesco Dagnino and Elena Zucca 2018 Is Part Of LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ECOOP.2018.21 urn:nbn:de:0030-drops-92267 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.21 eng https://creativecommons.org/licenses/by/3.0/legalcode