Jeremy Siek, an associate professor at the School of Informatics, Computing, and Engineering, has been awarded a grant worth more than $380,000 by the National Science Foundation to revive and simplify the denotational semantics approach to programming language specification.
Software relies on compilers to automatically translate from the language in which people write software (e.g. Java, C++, etc.) to a language understood by a computer (e.g. Intel’s x86 assembly language). A mistake in a compiler for a language such as Java, for example, introduces bugs in all Java programs, so it is imperative for compilers to be correct. The state-of-the-art techniques, using so-called operational semantics, currently require up to 10 years of work to guarantee that a compiler is correct.
Denotational semantics, initially developed 50 years ago, offers an alternative approach that maps each language feature to a precise mathematical entity, but it fell out of use because of its complexity. Siek realized that this overlooked approach could drastically reduce the time needed to establish compiler correctness.
“I was conducting research on Gradual Typing looking for techniques to help specify the behavior of values as they pass from a region of dynamically typed code into a region of statically typed code,” Siek said. “I read about denotational semantics and realized they are not inherently complex after all and enable substantial simplifications compared to prior approaches.”
Siek discovered that the use of elementary denotational semantics, which use simple mathematics, can be useful for the day-to-day work of language specification, mechanization, and complier correctness. He will use the grant to explore how to expand the denotational semantics approach to practical languages and to proving the correctness of their compilers.
“This grant will help us push our work forward in a way that can really improve the efficiency and security of software,” Siek said.
Siek’s grant will extend for the next three years.
“Ensuring a program does what the programmer thinks it will do is essential in a world where everything, from your phone to your self-driving car, relies on computer programs,” said Kay Connelly, the associate dean for research at SICE. “Jeremy’s work will help reduce the number of errors by making sure bugs aren’t introduced in the compilation process.”