Since 2015, I've been a programming languages researcher working on Syndicate, an actor-based language oriented around publish/subscribe communication.
I'm interested in the role that protocols play in program design and implementation. For many programs, and especially those requiring concurrency, the protocols of communication between components are as important as the components themselves. Yet, most programming languages provide little if any support for the design, implementation, and verification of these protocols.
My work on Syndicate has pursued using a type system as the avenue for introducing explicit support for protocols to the language. To achieve this, I first designed a type system for Syndicate that captures the essence of its form of publish/subscribe communication. I then extended this basic design with a type-and-effect system that captures the communication behaviors of the actors in a program. This communication specification is then compiled into the input language of a model checker, which verifies the program with respect to specifications of its protocols.