A joint research team from University of California San Diego and Microsoft Research received the Most Influential Paper Award at the 29th ACM SIGPLAN International Conference on Functional Programming (ICFP) held earlier this month in Milan, Italy.
Professor Ranjit Jhala and two alumni from the Jacobs School of Engineering’s Department of Computer Science and Engineering, Niki Vazou (PhD ’16) and Eric L. Seidel (M.S., PhD ’16, ’17), were among those recognized for the transformative paper, Refinement Types for Haskell. The paper was selected from 10 years of ICFP research for its influence over the past decade and for solving real-world problems in Functional Programming.
In their 2014 work, Jhala and his colleagues utilized advances in Satisfiability Modulo Theories (SMT) solving to build automated refinement type-based verifiers for Haskell, an advanced functional programming language designed to cope with large-scale applications in academia, research, and industry.
Their research exceeded classic SMT-based checking of refinement types for call-by-value languages by challenging the implicit assumption that all the free variables in the expression are bound to values. Alternatively, they proposed a stratified type system – one they dubbed LIQUIDHASKELL – that takes into account which subset of binders actually reduces to values.
The 2014 paper was one of 28 papers accepted at the 19th ACM ICFP, and has since been cited 211 times. It has also informed five subsequent studies by Jhala and colleagues, including ICFP papers in 2015 and 2017, Bounded Refinement Types and Local Refinement Typing, and a 2021 paper STORM: Refinement Types for Secure Web Applications, presented at the 15th USENIX Symposium on Operating Systems Design and Implementation.
ICFP is a forum for researchers, developers, and students to discuss the latest work on the design, implementation, principles, and use of functional programming. The conference covers the entire spectrum of work, from practice to theory.
--By Kimberley Clementi