Programming languages, particularly semantics and type systems for reasoning about imperative code, concurrency, security, compiler transformations, and provenance. Current focus is on correct and secure compilation, gradual typing, and safe language interoperability.