Gradual Typing for Effect Handlers

Explore a conference talk from OOPSLA 2023 that presents GrEff, a gradually typed language with effects and handlers supporting migration from unchecked to checked effect typing. Delve into the integration of effect typing discipline with existing effectful typed languages, and learn about the simple module system modeled after Typed Racket's gradual migration approach. Examine the semantics of GrEff through its elaboration to Core GrEff, and understand the inequational theory for reasoning about semantic error ordering and program equivalences. Discover how the operational semantics are derived from provable equations in the theory, and investigate the construction of an operational logical relations model to prove the graduality theorem. Gain insights into the extension of embedding-projection pair models of gradual typing to handle effect typing and subtyping in this 18-minute presentation by researchers from the University of Michigan and Wesleyan University.