Asynchronous Probabilistic Couplings in Higher-Order Separation Logic

Simon Oddershede Gregersen; Alejandro Aguirre; Philipp G. Haselwarter; Joseph Tassarotti; Lars Birkedal

doi:10.1145/3632868

Asynchronous Probabilistic Couplings in Higher-Order Separation Logic

Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal

Institut for Datalogi

Publikation: Bidrag til tidsskrift/Konferencebidrag i tidsskrift /Bidrag til avis › Tidsskriftartikel › Forskning › peer review

7 Citationer (Scopus)

Abstract

Probabilistic couplings are the foundation for many probabilistic relational program logics and arise when relating random sampling statements across two programs. In relational program logics, this manifests as dedicated coupling rules that, e.g., say we may reason as if two sampling statements return the same value. However, this approach fundamentally requires aligning or "synchronizing"the sampling statements of the two programs which is not always possible. In this paper, we develop Clutch, a higher-order probabilistic relational separation logic that addresses this issue by supporting asynchronous probabilistic couplings. We use Clutch to develop a logical step-indexed logical relation to reason about contextual refinement and equivalence of higher-order programs written in a rich language with a probabilistic choice operator, higher-order local state, and impredicative polymorphism. Finally, we demonstrate our approach on a number of case studies. All the results that appear in the paper have been formalized in the Coq proof assistant using the Coquelicot library and the Iris separation logic framework.

Originalsprog	Engelsk
Artikelnummer	26
Tidsskrift	Proceedings of the ACM on Programming Languages
Vol/bind	8
Nummer	POPL
ISSN	2475-1421
DOI	https://doi.org/10.1145/3632868
Status	Udgivet - jan. 2024

Adgang til dokumentet

10.1145/3632868Licens: Ikke-specificeret

Citationsformater

@article{ab25a5365dd642adab4a20d9eb6cedb2,

title = "Asynchronous Probabilistic Couplings in Higher-Order Separation Logic",

abstract = "Probabilistic couplings are the foundation for many probabilistic relational program logics and arise when relating random sampling statements across two programs. In relational program logics, this manifests as dedicated coupling rules that, e.g., say we may reason as if two sampling statements return the same value. However, this approach fundamentally requires aligning or {"}synchronizing{"}the sampling statements of the two programs which is not always possible. In this paper, we develop Clutch, a higher-order probabilistic relational separation logic that addresses this issue by supporting asynchronous probabilistic couplings. We use Clutch to develop a logical step-indexed logical relation to reason about contextual refinement and equivalence of higher-order programs written in a rich language with a probabilistic choice operator, higher-order local state, and impredicative polymorphism. Finally, we demonstrate our approach on a number of case studies. All the results that appear in the paper have been formalized in the Coq proof assistant using the Coquelicot library and the Iris separation logic framework.",

keywords = "Logical Relations, Probabilistic Couplings, Separation Logic",

author = "Gregersen, {Simon Oddershede} and Alejandro Aguirre and Haselwarter, {Philipp G.} and Joseph Tassarotti and Lars Birkedal",

note = "Publisher Copyright: {\textcopyright} 2024 Owner/Author.",

year = "2024",

month = jan,

doi = "10.1145/3632868",

language = "English",

volume = "8",

journal = "Proceedings of the ACM on Programming Languages ",

issn = "2475-1421",

publisher = "Association for Computing Machinery",

number = "POPL",

}

TY - JOUR

T1 - Asynchronous Probabilistic Couplings in Higher-Order Separation Logic

AU - Gregersen, Simon Oddershede

AU - Aguirre, Alejandro

AU - Haselwarter, Philipp G.

AU - Tassarotti, Joseph

AU - Birkedal, Lars

PY - 2024/1

Y1 - 2024/1

N2 - Probabilistic couplings are the foundation for many probabilistic relational program logics and arise when relating random sampling statements across two programs. In relational program logics, this manifests as dedicated coupling rules that, e.g., say we may reason as if two sampling statements return the same value. However, this approach fundamentally requires aligning or "synchronizing"the sampling statements of the two programs which is not always possible. In this paper, we develop Clutch, a higher-order probabilistic relational separation logic that addresses this issue by supporting asynchronous probabilistic couplings. We use Clutch to develop a logical step-indexed logical relation to reason about contextual refinement and equivalence of higher-order programs written in a rich language with a probabilistic choice operator, higher-order local state, and impredicative polymorphism. Finally, we demonstrate our approach on a number of case studies. All the results that appear in the paper have been formalized in the Coq proof assistant using the Coquelicot library and the Iris separation logic framework.

AB - Probabilistic couplings are the foundation for many probabilistic relational program logics and arise when relating random sampling statements across two programs. In relational program logics, this manifests as dedicated coupling rules that, e.g., say we may reason as if two sampling statements return the same value. However, this approach fundamentally requires aligning or "synchronizing"the sampling statements of the two programs which is not always possible. In this paper, we develop Clutch, a higher-order probabilistic relational separation logic that addresses this issue by supporting asynchronous probabilistic couplings. We use Clutch to develop a logical step-indexed logical relation to reason about contextual refinement and equivalence of higher-order programs written in a rich language with a probabilistic choice operator, higher-order local state, and impredicative polymorphism. Finally, we demonstrate our approach on a number of case studies. All the results that appear in the paper have been formalized in the Coq proof assistant using the Coquelicot library and the Iris separation logic framework.

KW - Logical Relations

KW - Probabilistic Couplings

KW - Separation Logic

U2 - 10.1145/3632868

DO - 10.1145/3632868

M3 - Journal article

AN - SCOPUS:85182283254

SN - 2475-1421

VL - 8

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

IS - POPL

M1 - 26

ER -

Asynchronous Probabilistic Couplings in Higher-Order Separation Logic

Abstract

Adgang til dokumentet

Fingeraftryk

Citationsformater