Institute of Cybernetics at TUT
Thursday, 3 November 2011, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101
Abstract: Big-step operational semantics are nice compared to small-step semantics because of their (near-)compositionality, making them particularly well-suited for reasoning about programs. But standard big-step semantics do not account for nonterminating program behaviors, these are simply ignored.
In this talk, I show how to develop trace- and resumption-based big-step semantics free of this serious drawback, based on coinductive types and predicates. I will consider a simple imperative language and its extensions for interactive input-output and concurrency.
(To a large part, joint work with Keiko Nakata.)