Speaker:Swarn Priya

Major Professor:  Ciardo, Gianfranco
Committee Member 1:  Basu, Samik
Committee Member 2:  Kautz, Steve

Status:  MS Final Oral
Date: Wed, 2017-11-08
Time: 5:20 pm
Location: Atanasoff Hall 216

Title: λir: A Language with Intensional Receive
Abstract: Message passing-based programming is one of the dominant concurrent
programming models today in both research and practice.
The major challenge in message passing concurrency is to reason about the
type of message received by any process and its effect.
We present λir, a message passing-based language that incorporates an
intensional design of the receive expression to solve this problem.
Intensional design of receive expression integrates static and dynamic type
checking and allows the effect of the message received to be
intensionally inspected through a notion of dynamic typing. This enables
reasoning about the effect of the message received from the head
of the mailbox while retaining static type safety. We demonstrate the
applications of intensional design of receive expression in various
programming patterns like multiplexing, safe pipelining, encoding state
machines, supporting the chain of responsibility pattern and error handling.
In each of these applications, intensional receive helps in providing better
safety. We have also formalized λir using the Coq proof assistant and prove
its soundness.