works on

From the 1 of 8 linked papers with an AI index.

activity
20242026
most citedContextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)

1 citations · 1 across the 3 of their papers we have counts for

collaborators

8 papers

cs.LO2026

Elton: Urn Resources for Reasoning about Adversarial Probabilistic Programs

Kwing Hei Li, Alejandro Aguirre, Philipp G. Haselwarter +2

The paper presents Elton, a higher-order separation logic for reasoning about probabilistic programs that may contain unknown adversarial code, introducing urn resources and delaye…

cs.LO2026

Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic

Markus de Medeiros, Puming Liu, Kwing Hei Li +3

Most implementations of sampling algorithms for continuous distributions use floating-point numbers, which introduce round-off errors and approximations. These errors can be diffic…

cs.LO20261 cited

Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)

Kwing Hei Li, Alejandro Aguirre, Joseph Tassarotti +1

We present Foxtrot, the first higher-order separation logic for proving contextual refinement of higher-order concurrent probabilistic programs with higher-order local state. From…

cs.PL2026

Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Extended Version)

Philipp G. Haselwarter, Alejandro Aguirre, Simon Oddershede Gregersen +3

Differential privacy is the standard method for privacy-preserving data analysis. The importance of having strong guarantees on the reliability of implementations of differentially…

cs.LO2025

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)

Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen +3

We present Coneris, the first higher-order concurrent separation logic for reasoning about error probability bounds of higher-order concurrent probabilistic programs with higher-or…

cs.LO2024

Approximate Relational Reasoning for Higher-Order Probabilistic Programs

Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre +3

Properties such as provable security and correctness for randomized programs are naturally expressed relationally as approximate equivalences. As a result, a number of relational p…