Apr 6, 2014
Peter Thiemann: Session Types with Gradual Types
Session types enable fine-grained static control over communication
protocols. Gradual typing is a means
to safely integrate statically and dynamically-typed program fragments.
We propose a calculus for synchronous functional two-party session
types, augment this calculus with a dynamically-typed fragment as
well as coercion operations between statically and dynamically-typed
parts, and establish its basic metatheory: type preservation and progress.
We explore two different representations for coerced communication
channels, with eager and lazy cast semantics. The lazy version is
more efficient, but requires coercion simplification to establish the
metatheory.