2 papers
cs.LO2025
Logical Relations for Formally Verified Authenticated Data Structures
Simon Oddershede Gregersen, Chaitanya Agarwal, Joseph Tassarotti
Authenticated data structures allow untrusted third parties to carry out operations which produce proofs that can be used to verify an operation's output. Such data structures are…
cs.PL2018
A Separation Logic for Concurrent Randomized Programs
Joseph Tassarotti, Robert Harper
We present Polaris, a concurrent separation logic with support for probabilistic reasoning. As part of our logic, we extend the idea of coupling, which underlies recent work on pro…