Colloquium Details
Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While
| Author: | Keiko Nakata Institute of Cybernetics at Tallinn University of Technology |
|---|---|
| Date: | February 10, 2011 |
| Time: | 15:30 |
| Location: | 220 Deschutes |
| Host: | Zena Ariola |
Abstract
In search for a foundational framework for reasoning about observable behavior of programs that may not terminate, we have previously devised a coinductive operational semantics for While. The operational semantics keeps track of all the states that an execution goes through as a trace (a possibly infinite sequence of states). The trace is finite for a terminating execution and infinite for a non-terminating execution. Subsequently we designed a Hoare logic counterpart of our coinductive trace-based semantics and proved it sound and complete. Our logic subsumes both the partial correctness Hoare logic and the total correctness Hoare logic: they are embeddible. All the results have been formalized in Coq constructively.
In this talk, I will overview the coinductive operational semantics and the Hoare logic, aiming at delivering the intuition behind.
(Joint work with Tarmo Uustalu.)
Biography
Keiko Nakata is a senior researcher at Institute of Cybernetics, Tallinn University of Technology, Estonia. Her work is concerned around programming language semantics and constructive mathematics. She received her Ph.D. in 2007 from the Research Institute for Mathematical Sciences, Kyoto University, Japan.