Modeling infinite behaviour by corules
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.
Fri 20 JulDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 17:15 | |||
16:00 25mResearch paper | FHJ: A Formal Model for Hierarchical Dispatching and Overriding ECOOP Research Papers Yanlin Wang University of Hong Kong, Haoyuan Zhang , Bruno C. d. S. Oliveira University of Hong Kong, China, Marco Servetto Victoria University of Wellington DOI | ||
16:25 25mResearch paper | Modeling infinite behaviour by corules ECOOP Research Papers Davide Ancona University of Genova, Francesco Dagnino DIBRIS, University of Genova, Italy, Elena Zucca University of Genova DOI | ||
16:50 25mResearch paper | The Essence of Nested Composition ECOOP Research Papers Xuan Bi The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong, China, Tom Schrijvers KU Leuven DOI |