Recent MMath graduate Jason Hu and Cheriton School of Computer Science Professor Ondřej Lhoták have received a Distinguished Paper Award at POPL 2020, the 47thACM SIGPLAN Symposium on Principles of Programming Languages.
Held this year in New Orleans, Louisiana from January 19 to 25, POPL 2020 is the premier symposium to discuss all aspects of programming languages and programming systems on topics from formal frameworks to experience reports. In particular, submissions are sought that make principled, enduring contributions to the theory, design, understanding, implementation or application of programming languages.
Their paper, titled Undecidability of D<: and Its Decidable Fragments, presented a proof of undecidability for the D<: calculus. This work not only confirmed a previously conjectured result that both typing and subtyping of D<: are undecidable, but it also demonstrated that previous arguments made in support of the conjecture were insufficient as a proof.
“Jason and Ondřej’s results are theoretical, but they have real, practical applications to the implementation of subtyping in Scala,” said Mark Giesbrecht, Director of the David R. Cheriton School of Computer Science. “Even more impressive is that their proofs have been fully mechanized using proof assistants — Coq for correctness proofs and Agda for proofs of undecidability.”
“I am happy to let you know that your paper has been selected to receive a Distinguished Paper Award,” wrote Lars Birkedal, POPL 2020 Program Chair, in his email to Professor Lhoták. “This award highlights papers that the POPL program committee thinks should be read by a broad audience due to their relevance, originality, significance and clarity.”
This year, 68 papers were accepted at POPL 2020, of which six were selected to receive a Distinguished Paper Award.
