Resumption-based big-step and small-step interpreters for While with interactive I/O
Keiko Nakata (Institute of Cybernetics at Tallinn University of, Technology)

TL;DR
This paper develops big-step and small-step interpreters for the While language with interactive I/O, using traces and resumptions to model program behavior, including non-termination, within a constructive type theory framework.
Contribution
It introduces a novel approach to interpreters for While with I/O by employing trace-based and resumption-based semantics, extending previous work to handle interactive features.
Findings
Trace-based interpreters model program execution and non-termination.
Resumption-based interpreters handle interactive input/output.
The approach is grounded in constructive type theory.
Abstract
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 consisting of skip, assignment, sequence, conditional and loop. We first develop trace-based interpreters for While. Traces are potentially infinite nonempty sequences of states. The interpreters assign traces to While programs: for us, traces are denotations of While programs. The trace is finite if the program is terminating and infinite if the program is non-terminating. However, we cannot decide (i.e., write a program to determine), for any given program, whether its trace is finite or infinite, which amounts to deciding the halting problem. We then extend While with interactive input/output primitives. Accordingly, we extend the interpreters by generalizing traces to resumptions. The tutorial is based on…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
