Thursday, 13 May 2010, 16:00 (note the unusual time!)
Cybernetica Bldg (Akadeemia tee 21), room B401
Slides from the talk [pdf]
Abstract: We study the question of how to design big-step semantic descriptions for languages where programs need not terminate, but some actions they perform (like interactive I/O) are observable. This is relevant, e.g., in compiler correctness and program verification. We look at the problem through the glasses of constructive type theory.
We define several big-step semantics of a suitable extension of While, based on resumptions and termination-sensitive weak bisimilarity.
After first considering a basic semantics of statements in terms of resumptions with explicit internal actions (delays), we introduce a a variation where resumptions are delay-free: essentially, finite sequences of delays are removed on the fly from those resumptions that are responsive (keep performing observable actions every now and then). We also look at a semantics where delay-free resumptions are augmented with a silent divergence option. This variation hinges on ahead-of-time commitments between convergence and divergence. Classically, it is equivalent to the basic one.
The whole enterprise is an exercise in mixing induction and coinduction, which is interesting both mathematically and from the point-of-view of implementing it in a proof assistant. We have fully formalized our development in Coq.
Joint work with Keiko Nakata.