10 citations · 27 across the 10 of their papers we have counts for
5 papers · 1 filter
Modelling Recursion and Probabilistic Choice in Guarded Type Theory
Philipp Jan Andries Stassen, Rasmus Ejlers Møgelberg, Maaike Zwart +2
Constructive type theory combines logic and programming in one language. This is useful both for reasoning about programs written in type theory, as well as for reasoning about oth…
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…
Tachis: Higher-Order Separation Logic with Credits for Expected Costs
Philipp G. Haselwarter, Kwing Hei Li, Markus de Medeiros +4
We present Tachis, a higher-order separation logic to reason about the expected cost of probabilistic programs. Inspired by the uses of time credits for reasoning about the running…
Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros +4
Probabilistic programs often trade accuracy for efficiency, and thus may, with a small probability, return an incorrect result. It is important to obtain precise bounds for the pro…
Almost-Sure Termination by Guarded Refinement
Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter +2
Almost-sure termination is an important correctness property for probabilistic programs, and a number of program logics have been developed for establishing it. However, these logi…