Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus

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

Documents

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 languageEnglish
Title of host publication27th European Symposium on Programming, ESOP 2018
EditorsAmal Ahmed
Number of pages28
PublisherSpringer VS
Publication year18 Apr 2018
Pages214-241
ISBN (print)9783319898834
DOIs
StatePublished - 18 Apr 2018
EventETAPS 2018 - Thessaloniki, Greece
Duration: 14 Apr 201820 Apr 2018
https://www.etaps.org/

Conference

ConferenceETAPS 2018
LandGreece
ByThessaloniki
Periode14/04/201820/04/2018
Internetadresse
SeriesLecture Notes in Computer Science (LNCS)
Number10801
ISSN0302-9743

See relations at Aarhus University Citationformats

ID: 123471792