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 Jul (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
|13:50 - 14:20|
|14:20 - 14:50|
|14:50 - 15:20|