We face the problem of providing a denotational semantics for corecursive methods with default, a programming feature for manipulating cyclic structures without ad-hoc machinery. To this aim, we study new lattices for which the theorem of Kleene is applicable so that the semantics of a corecursive method with default corresponds to the greatest fixed point computed as the greatest lower bound of a descending chain. The proposed definition allows us to prove correctness of some kinds of corecursive methods. This solution is only partly satisfactory, and a different and more general approach is currently under development.
Tue 19 JulDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:50 - 15:20
|Generating Concurrency Checks Automatically|
|An Extended Buffered Memory Model With Full Reorderings|
|Towards a Model of Corecursion with Default|