Amal Ahmed, an assistant professor in the College of Computer and Information Science, was recently awarded a $500,000 National Science Foundation grant for a proposal titled “CAREER: Verified Compilers for a Multi-Language World.”

“I would describe it as extremely ambitious,” Ahmed, who has been at Northeastern since 2011, says of her proposal. “This is something that’s really hard to do – getting different languages to come together, and to do that in the context of compiler correctness is very, very hard.”

The award comes from the NSF’s Faculty Early Career Development Program, which recognizes junior faculty for their contributions to education and research within their institutions. Researchers submit their proposals for peer-review by a panel of experts who make recommendations for awards. Ahmed says that the most valuable part of receiving the honor was reading the comments from her community: “That’s really the best part about it. Reading some of the reviews is so heartening.”

Ahmed’s research tackles a problem that that has long existed in the computer science community. When programmers write code, they generally use high-level languages like Java that need to be translated by compilers before a computer can interpret the code. As a result, there needs to be proof of equivalence – some proof that the source code written by programmers results in the same outcome as target code produced by the compiler.

The complications arise from the fact that compilers require complete programs in order to guarantee accurate translation, but it is rare that a program is written in a single language. Instead, the program might be a collection of various languages, such as Java, a typed language, and C, an unsafe language. Typed languages come with more guarantees and give programmers more certainty about the behavior of programs. For example, private fields in Java allow programmers to keep some information private from client components, keeping confidential data from being leaked. But unsafe languages like C don’t come with those safeguards, and linking two programming languages could result in the loss of the guarantees from the typed language.

This is among the issues that Ahmed’s research wrestles with. Her recent work has looked at interoperability between different programming languages – making sure that the languages work together without compromising their individual properties. The proposal for which she was awarded the NSF award is a two-part approach to the problem: first, proving compiler correctness for components of a program from different languages, and second, putting code from different languages together at a target level.

“My whole thesis in this proposal is that compiler correctness is a language interoperability problem,” she says. “We can’t really solve compiler correctness for a world of multi-language software without thinking about and acknowledging that there’s language interoperability issues that need to be addressed.”

– As seen in the April 2015 E-Newsletter –