Yale-NUS Associate Professor Ilya Sergey wins prestigious Distinguished Paper Award at top-tier computer science conference

Yale-NUS Associate Professor of Science (Computer Science) Ilya Sergey. Image provided by Assoc Prof Sergey.

Yale-NUS faculty frequently make waves in their academic fields, contributing to scholarship and developing innovative ways of thinking about research problems. Many have received peer recognition for their work and Associate Professor of Science (Computer Science) Ilya Sergey is no exception. Assoc Prof Sergey recently received the Distinguished Paper Award at the 42nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) in 2021.

“PLDI is a premier forum in the field of programming languages and programming systems research, covering the areas of design, implementation, theory, applications, and performance,” Assoc Prof Sergey shared. The conference is sponsored by the Association for Computing Machinery’s Special Interest Group on Programming Languages (SIGPLAN), an acclaimed organisation in the field of computer science.

The annual conference, which was held virtually from 20 to 25 June 2021, comprised a series of talks, workshops, and tutorial sessions, as well as an opportunity for researchers across the globe to submit research papers on their latest work. Assoc Prof Sergey said, “A total of 320 papers were submitted to the conference and 87 were accepted. Our paper was one out of eight that won the Distinguished Paper Award.”

He shared that the paper was co-authored with four other researchers from various universities around the world.

The co-authors of the paper, Hila Peleg from the Technion–Israel Institute of Technology, Reuben N.S. Rowe from the Royal Holloway, University of London, Nadia Polikarpova from the University of California, San Diego, and Shachar Itzhaky from Technion–Israel Institute of Technology (left to right). Images provided by Assoc Prof Sergey.

“In our work titled ‘Cyclic Program Synthesis’, we have advanced the state of the art in deductive program synthesis — an approach to automatically generate correct-by-construction programs from their concise logical specifications,” he shared.

Program synthesis is the process of automatically constructing a program that meets a given specification, and proofs are used to demonstrate that a given program does what is required by the specification. The team’s project had solved a long-standing challenge that has been beyond the reach for existing approaches for program synthesis. “We have developed a novel methodology to synthesise heap-manipulating programs that rely on arbitrary auxiliary recursive procedures. The key enabling component of our work is the idea of enhancing program synthesis with cyclic proofs — a powerful reasoning mechanism from the line of work on automated theorem proving,” he said.

“Yale-NUS students who took classes such as “Introduction to Computer Science” or “Introductory Data Structures and Algorithms” should be very familiar with such programs, which are standard solutions for problems like transforming a binary tree data structure into a list. While the students learn how to implement those programs from scratch in OCaml (a type of programming language), our approach makes it possible to generate them completely automatically from concise problem descriptions,” he added.

The team implemented their work in a programming tool called Cypress, which automates the generation of certain important programs and tasks. “Cypress is very fast, and it can synthesise many programs within a few seconds on a commodity laptop,” he added. The tool has also been made publicly online for other programmers.

Assoc Prof Sergey’s work on this topic has been several years in the making, with its origins as a collaborative effort between him, Professor Nadia Polikarpova from the University of California, San Diego, and their respective research laboratories. “This work continues a long-term research agenda on developing practical methodologies for program synthesis of provably correct programs in languages such as C and Rust,” he said.

The research team is also planning for the future, with further applications of their research planned to target automatic repair of vulnerabilities in real-world software, automated assessment of programming assignments, and building tools for synthesis-aided programming.

Even before PLDI 2021, students at Yale-NUS have been interested in Assoc Prof Sergey’s work on the topic and have even developed their own spin-offs in their capstone dissertations. Yasunari Watanabe (Class of 2020), a Mathematical, Computational, and Statistical Sciences major, completed his capstone titled “Building a Certified Program Synthesiser” under Assoc Prof Sergey’s supervision. He also won the Outstanding Yale-NUS Capstone Prize in 2020 for his project.

Aside from his work at Yale-NUS, Assoc Prof Sergey holds a joint appointment at the School of Computing at the National University of Singapore (NUS). He also runs the Verified Systems Engineering (VERSE) Research Lab at NUS which does research in the design and implementation of programming languages, mathematical models of computation, and computer-assisted formal reasoning.