Staff

Over the years, I have worked on a variety of problems associated with semantics of programming languages. Here is a selected list, in roughly reverse chronological order: probabilistic programming languages, binding-safe programming, aspect-oriented programming, analysis-based program transformation, compiler correctness proofs, continuations, macros.

My current research is about using deep reinforcement learning and Monte Carlo Tree Search (a Google/DeepMind algorithm) to synthesize instance-based programs to solve problems formulated in interpreted first-order logic, e.g., algorithmic problems. My earlier work in programming methodology centers on using (1) context-free grammars for abstract data types and domain-specific languages (the Demeter Method); (2) a succinct and exact definition of a detector for an interesting class of software design problems: The Law of Demeter (Don't Talk to Strangers); it allows for a direct application when writing object-oriented code; (3) aspect-oriented programming. I am also interested in problem-solving methodology in algorithms and I helped to develop the classical golden-ratio result for Satisfiability.

I explore all aspects of program design and programming language design. My current research involves work on behavioral software contracts, gradual typing of scripting languages, language interoperability, language extensibility, and module systems. I also engage in educational outreach work. For the past 20 years, I have worked with middle schools, high schools, after-school programs, and college faculty on injecting design ideas into mathematics and computer science courses. Such educational interactions often inspire our research, and many research efforts end up improving my educational work.

My principal research interests include the construction of robust, complex software artifacts and the design of tools that assist programmers in this task; the interaction between systems and programming languages, primarily higher-order typed languages; the design and analysis of programming languages; and compilers. Before coming to Northeastern, I was a research scientist at MIT’s Artificial Intelligence Lab, a founder and CTO of the Smartleaf Corporation, and a faculty member at the Georgia Institute of Technology.

I work on problems involving semantics of programming languages, including advanced type systems for programs that manipulate memory, correct and secure compilation, gradual typing, and language interoperability. My prior work has shown how to scale the logical relations proof method to realistic languages. This technique has been used in numerous contexts, e.g., to prove compiler correctness, to verify concurrent code, to establish guarantees provided by type systems for confidentiality or differential privacy. My present focus is on how to build verified compilers that ensure safe linking of code compiled from different programming languages.

I have worked on problems in web programming semantics, including designing and analyzing extensibility mechanisms for browsers, studying the interactions between extensions and each other or with intended browser behavior. With colleagues at Brown, I have been helping to design and implement a language that focuses on the linguistic support needed for introductory-level pedagogy.

I work on the design and implementation of programming languages. I led the implementation of the first real-time Java virtual machine to be flight-tested. With Noble and Potter, I proposed what became known as Ownership Types. I tried to understand JavaScript by dynamic analysis and am now looking at supporting scalable data analysis in R.

My research is in the areas of Programming Languages and Software Engineering and is focused on the use of program analysis in tools that help increase programmer productivity and software quality. Specific topics that I've worked on in recent years include tools for detecting and localizing bugs, refactoring, test generation, and optimization.

I have broad interests in programming languages, but usually work on language-based approaches to security, reliability, and performance. I've spent several years thinking about JavaScript (semantics, type checking, static analysis, reactive programming, and more). I also spent several years working on programming languages for software-defined networking. These days, I study problems that arise in cloud computing, system configurations, and robotics, through the lens of programming languages.

I apply a systems perspective to software engineering challenges, observing the issues that developer face when creating reliable software, and then designing new mechanisms to support developers. My research focuses on improving existing developer-written tests, making them run faster and more reliably while amplifying them to be more comprehensive and also tracking their overall quality. Rather than focus solely on finding a handful of high-value “million dollar bugs” in a small pool of high-assurance software, my research aims to have very broad impacts, helping everyday developers just as much as experts.

My research focuses on programming languages and artificial intelligence. In particular, my goal is to use programming languages and program analysis techniques as a foundation for specifying and reasoning about probabilistic models. Towards this end I am interested in the design, implementation, and applications of probabilistic programming languages; foundations of probabilistic inference and tractable probabilistic modeling; automated reasoning; and probabilistic verification.

My work focuses on connections between logic and computer science, such as (dependent) type systems, logic programming, logical frameworks, and proof assistants. I use the lens of logic to understand fundamental principles of computation, motivated by supporting elegant abstractions for practitioners of creative endeavors such as mathematics, art, and game design.

I'm interested in language and type system interoperability — in particular, languages with very different type systems interacting easily and safely.

I use tools from the programming languages and verification literature to create systems with formally proven security guarantees. Among other things, I am interested in language-based approaches for giving state-of-the-art security guarantees to high-performance, cryptographic software.

I study computer systems using tools from programming languages and formal verification, especially domain-specific languages (DSLs). My PhD introduced mechanized semantics and certified translation validators for P4, a networking DSL. My postdoctoral research focuses on DSLs for hardware.

I find delight in programming languages that allow extension of their notation, syntactic forms, type systems, runtime behaviors, and development environments. My research aims to build the foundations needed to bring these extensibility features into widespread use.

I like reasoning about programming languages and compilers, using pencil and paper or proof assistants.

I enjoy flexible programming languages and elegant software. I'm interested in designing tools that enable everyday developers to build more robust programs.

I research probabilistic programming languages, specifically designing languages that let users fine-tune the (statistical) inference process.

I like types, proofs, and occasionally programs.

I like to design domain-specific languages with strong guarantees, which are usually supported by rich type systems and formal methods. My current research is on language-based security.

My research focuses on helping developers identify and correct software bugs and vulnerabilities.

I enjoy working on formalizing semantics of systems so as to uncover surprising behavior, and fix related bugs. Recently I'm working on understanding the semantics of package managers.

I like thinking about programming languages and compilers.

I really enjoy functional programming and would like to develop languages that allow for the use of functional programming techniques in areas that they have not been used before.

I like logic, semantics, and interactive theorem proving.

I am interested in program analysis and security. I am currently working on static analysis for JavaScript, and security in PLCs.

I completed my master's degree at University of Michigan, where I also developed an automated grading system that is used by over 5000 students per semester. My research interests lie at the intersection of PL and Software Engineering, and my current work is focused on mutation testing.

My interests are dynamic languages implementations, Just-in-time compilers, and WebAssembly.

I am interested in improving tools used by data scientists.

I’m interested in developing robust, performant Large Language Models for code that can be deployed with limited compute. I like taking apart transformer layers to interpret their inner workings.

I'm interested in program analysis and optimization.

I'm interested in property based testing, fuzzing, and testing of all kinds.

I'm interested in type systems, logic, dynamics, and abstract semantics for proving interesting properties about interesting programming languages.

I'm interested in developing approaches that enable both computers and humans to more easily reason about complex applications.

I like to work on programming languages, and software testing. I also enjoy thinking about specifications of distributed systems.

I primarily work on compilers, trying to make programs run fast, and I am also interested in adjacent fields like Programming Languages. Currently working on a compiler that produces parallel GPU code, so developers don't have to use C++ and think about hardware

I study linear logic and its relationship to other formalisms like planning.