Computer Science – Programming Languages
Scientific paper
2011-09-05
EPTCS 66, 2011, pp. 226-235
Computer Science
Programming Languages
In Proceedings DSL 2011, arXiv:1109.0323
Scientific paper
10.4204/EPTCS.66.12
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 our previous work with T. Uustalu on reasoning about interactive programs in the setting of constructive type theory.
No associations
LandOfFree
Resumption-based big-step and small-step interpreters for While with interactive I/O does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Resumption-based big-step and small-step interpreters for While with interactive I/O, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Resumption-based big-step and small-step interpreters for While with interactive I/O will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-449145