Distinguished paper at ICFP'24
The paper "Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs", co-authored by Alejandro Aguirre, Philipp G. Haselwarter, Kwing Hei Li, and Lars Birkedal, along with their collaborators from New York University (NYU), has been selected as a distinguished paper at this year's International Conference on Functional Programming (ICFP'24).
The paper introduces Eris, a novel higher-order separation logic designed to provide precise error probability bounds for probabilistic programs. By introducing the concept of error credits as a resource within the logic, the authors enable more accurate and modular reasoning about errors, improving upon existing verification approaches that often yield overly coarse bounds. This innovative method is demonstrated through applications such as analyzing collision probabilities in hash functions and proving the correctness of rejection sampling algorithms. The results have been fully mechanized in the Coq proof assistant, showcasing the robustness of the approach.
Click here to read the full paper.
Congratulations to the entire team on this outstanding achievement!