## Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

### DOI

Alejandro Aguirre, IMDEA Software Institute, Gilles Barthe, IMDEA Software Institute,
• Lars Birkedal
• Aleš Bizjak
• Marco Gaboardi, University at Buffalo State University of New York, Deepak Garg, MPI-SWS, Saarbruecken
We extend the simply-typed guarded $\lambda$-calculus with discrete probabilities and endow it with a program logic for reasoning about relational properties of guarded probabilistic computations. This provides a framework for programming and reasoning about infinite stochastic processes like Markov chains. We demonstrate the logic sound by interpreting its judgements in the topos of trees and by using probabilistic couplings for the semantics of relational assertions over distributions on discrete types. The program logic is designed to support syntax-directed proofs in the style of relational refinement types, but retains the expressiveness of higher-order logic extended with discrete distributions, and the ability to reason relationally about expressions that have different types or syntactic structure. In addition, our proof system leverages a well-known theorem from the coupling literature to justify better proof rules for relational reasoning about probabilistic expressions. We illustrate these benefits with a broad range of examples that were beyond the scope of previous systems, including shift couplings and lump couplings between random walks.
Original language English 27th European Symposium on Programming, ESOP 2018 Amal Ahmed 28 Springer VS 18 Apr 2018 214-241 9783319898834 10.1007/978-3-319-89884-1_8 Published - 18 Apr 2018 ETAPS 2018 - Thessaloniki, GreeceDuration: 14 Apr 2018 → 20 Apr 2018https://www.etaps.org/

### Conference

Conference ETAPS 2018 Greece Thessaloniki 14/04/2018 → 20/04/2018 https://www.etaps.org/
Series Lecture Notes in Computer Science (LNCS) 10801 0302-9743

Citationformats