34 citations · 50 across the 4 of their papers we have counts for
7 papers
A Hoare logic for the coinductive trace-based big-step semantics of While
Keiko Nakata, Tarmo Uustalu
In search for a foundational framework for reasoning about observable behavior of programs that may not terminate, we have previously devised a trace-based big-step semantics for W…
On streams that are finitely red
Marc Bezem, Keiko Nakata, Tarmo Uustalu
Mixing induction and coinduction, we study alternative definitions of streams being finitely red. We organize our definitions into a hierarchy including also some well-known altern…
A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators
Danko Ilik, Keiko Nakata
First, we reconstruct Wim Veldman's result that Open Induction on Cantor space can be derived from Double-negation Shift and Markov's Principle. In doing this, we notice that one h…
Resumption-based big-step and small-step interpreters for While with interactive I/O
Keiko Nakata
In this tutorial, we program big-step and small-step total interpreters for the While language extended with input and output primitives. While is a simple imperative language cons…
Resumptions, Weak Bisimilarity and Big-Step Semantics for While with Interactive I/O: An Exercise in Mixed Induction-Coinduction
Keiko Nakata, Tarmo Uustalu
We look at the operational semantics of languages with interactive I/O through the glasses of constructive type theory. Following on from our earlier work on coinductive trace-base…
Lazy mixin modules and disciplined effects
Keiko Nakata
Programming languages are expected to support programmer's effort to structure program code. The ML module system, object systems and mixins are good examples of language construct…