Shared memory provides a practical way for concurrently executing processes or threads to communicate, and is widely used as a result. But how do we safely work with shared memory in a functional language? Futures provide a partial answer by giving a form of write-once shared memory which is nevertheless expressive enough for many practical programs. However, futures, like many constructs for adding concurrency to a functional language, are unsatisfying from a foundational perspective, as they add a concurrent portion to a sequential base language in a somewhat ad hoc manner. We attempt to resolve this by providing a formal semantics for write-once shared memory that is logically grounded via a Curry-Howard type interpretation.
Presented in Partial Fulfillment of the CSD Speaking Skills Requirement.
Zoom Participation. See announcement.