I’m a software engineer at GitHub working on code intelligence technology that powers GitHub’s data and security products. Previously I completed my bachelor’s and master’s in computer science at the University of Cambridge, specialising in programming language theory and machine learning.
I’m interested in a broad range of topics within programming languages, machine learning, and their intersection: in my master’s I studied category theory, machine learning, metaprogramming, formal methods, and applying ML to software development. I researched polymorphic subtyping under the supervision of Neel Krishnaswami for my master’s dissertation, and implemented a systematic concurrency testing system for Multicore OCaml supervised by KC Sivaramakrishnan for my bachelor’s dissertation.
During my studies, I interned with a few different teams across Microsoft. Most recently, I interned with the Programming Languages and Software Engineering group at Microsoft Research. Before that, I worked on highly scalable infrastructure powering Office, and before that, I contributed to reducing Bing’s cost to serve.
Implicit Polarized F: local type inference for impredicativity. Henry Mercer, Cameron Ramsay, and Neel Krishnaswami.
System F, the polymorphic lambda calculus, features the principle of impredicativity: polymorphic types may be (explicitly) instantiated at other types, enabling many powerful idioms such as Church encoding and data abstraction. Unfortunately, type applications need to be implicit for a language to be human-usable, and the problem of inferring all type applications in System F is undecidable. As a result, language designers have historically avoided impredicative type inference.
We reformulate System F in terms of call-by-push-value, and study type inference for it. Surprisingly, this new perspective yields a novel type inference algorithm which is extremely simple to implement (not even requiring unification), infers many types, and has a simple declarative specification. Furthermore, our approach offers type theoretic explanations of how many of the heuristics used in existing algorithms for impredicative polymorphism arise.