Abstract:

A capsule is a pair (e,t), where e is a lambda-term and t is a partial function with finite domain from variables to irreducible lambda-terms such that (1) for all x in dom t, FV(t(x)) subset dom t, and (2) FV(e) subset dom t. Capsules provide an algebraic representation of the state of a computation in higher-order functional and imperative languages. They can be used to model closures or heap-allocated environments but are much simpler than either. A capsule is essentially a finite coalgebra representing a (possibly infinite) regular closed lambda-coterm. Recursive functions are represented directly without using fixpoint combinators, and all operations are typable with simple types, yet the system is Turing complete. Thus we avoid unnatural fixpoint combinators that are not simply typable and impose a call-by-name discipline. I will describe an operational semantics based on capsules for a simple functional/imperative language with mutable variables and show that it adequately captures lexical scoping without any auxiliary combinatorial constructs such as stacks, heaps, or closures.

(Joint work with Jean-Baptiste Jeannin, Cornell.)