CMU-CS-15-130
Computer Science Department
School of Computer Science, Carnegie Mellon University


CMU-CS-15-130

Practical and Safe Abstractions for
Interactive Computation via Linearity

Stefan K. Muller, William A. Duff, Umut A. Acar

August 2015

CMU-CS-15-130.pdf


This is a version of a paper that was submitted to the
42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2015)
in July 2014.

Apart from typographical corrections, the difference between the July 2014 submission and this technical report
concerns terminology: here, we use the term "factor" instead of "interactible".
We also include some proof details that were omitted from the submission for space reasons,
and have made one minor correction as noted in the text.


Keywords: Interaction, reactive programming, equational reasoning, linear type systems

We propose abstractions and techniques for interactive or reactive computation that are general-purpose, expressive, flexible, and that can enable writing efficient interactive programs. Our key interactivity abstraction is a factor: a co-inductive type that abstracts interaction as exchange of information and internal state change. To enable expressive and flexible development of interactive programs, we extend a linearly typed, call-by-value lambda calculus with factors as first-class values. The resulting language, called λi, allows input and output through factors that reflect the changing state of the world. To ensure correctness and efficiency in the presence of such effects, λi treats interaction as a consumable, linear resource. The small-step semantics of λi takes advantage of the linearity to prevent unsafe behavior as well as guarantee efficiency. We formalize λi, and establish its type safety and additional meta-theoretical results that show that interaction and purely functional programming are not always inconsistent. We formalize all of our results in the Coq proof assistant. We give an implementation of λi as an OCaml library along with a relatively broad range of example applications.

35 pages

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by [email protected]