Sophisticated domain-specific and user-defined notation is widely used in formal models, but is poorly supported by proof assistants. This notation provides informal extensions to formal model that aid in communicating and reasoning about key ideas. Unfortunately, proof assistants do not allows users to conveniently define sophisticated notation. For instance, in modeling a programming language, we often define infix relations such as Γ ⊢ e : t and use BNF notation to specify the syntax of the language. In a proof assistant like Coq or Agda, users can easily define the notation for Γ ⊢ e : t , but to use BNF notation the user must use a preprocessing tool external to the proof assistant, which is cumbersome. To support sophisticated user-defined notation, we propose to use language extension as a fundamental part of the design of a proof assistant. We describe how to design a proof assistant that support safe, convenient, and sophisticated user-defined extensions, and show how language extension gives users the power to implement features of contemporary proof assistants.

I am a fifth year Ph.D. student at Northeastern University where I study Computer Science (specifically, programming languages).

The promise of programming languages research has been to provide high-level languages in which programmers can easily write complex programs without worrying about speed or low-level machine details. I think we have failed. Languages that provide strong guarantees are bemoaned as too complicated, compilers ignore those high-level guarantees anyway, and the folklore persists that C is the only language useful for writing fast code.

I want to make programs easier to design, write, and understand. To that end, I work on verifying compilers. I am particularly interested in equivalence preserving (fully-abstract) compilers. I also dabble in dependent types and compiler design and implementation.