Abstract

There are still many open problems in gradual typing. While there seems to be a fairly common static semantics the Gradually-Typed Lambda Calculus, there are a myriad of dynamic semantics all aimed at solving various problems that occur when you start mixing static and dynamic types. I will talk informally about the motivations for various dynamic semantics, explain how they relate to and differ from one another, and talk about open problems with each of them. I will then introduce the compiler that I am working on for the GTLC and my hopes for what we may learn from it.