Coinductive big-step semantics

Tarmo Uustalu

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.)

Tarmo Uustalu
Last update 2.11.2011