Playful, streamlike computation

TL;DR

This paper explores streamlike, interactive computation of sequential programs, tracing historical developments from Berry's work to modern game semantics, emphasizing the semantics of control operators and linear logic connections.

Contribution

It provides a survey of the evolution of sequential algorithms and streamlike computation, highlighting key insights and their impact on programming language semantics.

Findings

Streamlike computation allows interactive access to program semantics.

Sequential algorithms provide a direct semantics for control operators.

Connections to linear logic and game semantics have advanced understanding of sequentiality.

Abstract

We offer a short tour into the interactive interpretation of sequential programs. We emphasize streamlike computation -- that is, computation of successive bits of information upon request. The core of the approach surveyed here dates back to the work of Berry and the author on sequential algorithms on concrete data structures in the late seventies, culminating in the design of the programming language CDS, in which the semantics of programs of any type can be explored interactively. Around one decade later, two major insights of Cartwright and Felleisen on one hand, and of Lamarche on the other hand gave new, decisive impulses to the study of sequentiality. Cartwright and Felleisen observed that sequential algorithms give a direct semantics to control operators like \"call-cc\" and proposed to include explicit errors both in the syntax and in the semantics of the language PCF. Lamarche (unpublished) connected sequential algorithms to linear logic and games. The successful program of games semantics has spanned over the nineties until now, starting with syntax-independent characterizations of the term model of PCF by Abramsky, Jagadeesan, and Malacaria on one hand, and by Hyland and Ong on the other hand.