Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus

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

Standard

Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. / Aguirre, Alejandro; Barthe, Gilles; Birkedal, Lars; Bizjak, Aleš; Gaboardi, Marco; Garg, Deepak.

27th European Symposium on Programming, ESOP 2018. ed. / Amal Ahmed. Springer VS, 2018. p. 214-241 (Lecture Notes in Computer Science (LNCS); No. 10801).

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

Harvard

Aguirre, A, Barthe, G, Birkedal, L, Bizjak, A, Gaboardi, M & Garg, D 2018, Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. in A Ahmed (ed.), 27th European Symposium on Programming, ESOP 2018. Springer VS, Lecture Notes in Computer Science (LNCS), no. 10801, pp. 214-241, ETAPS 2018, Thessaloniki, Greece, 14/04/2018. https://doi.org/10.1007/978-3-319-89884-1_8

APA

Aguirre, A., Barthe, G., Birkedal, L., Bizjak, A., Gaboardi, M., & Garg, D. (2018). Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. In A. Ahmed (Ed.), 27th European Symposium on Programming, ESOP 2018 (pp. 214-241). Springer VS. Lecture Notes in Computer Science (LNCS), No. 10801 https://doi.org/10.1007/978-3-319-89884-1_8

CBE

Aguirre A, Barthe G, Birkedal L, Bizjak A, Gaboardi M, Garg D. 2018. Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. Ahmed A, editor. In 27th European Symposium on Programming, ESOP 2018. Springer VS. pp. 214-241. (Lecture Notes in Computer Science (LNCS); No. 10801). https://doi.org/10.1007/978-3-319-89884-1_8

MLA

Aguirre, Alejandro et al. "Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus". Ahmed, Amal (ed.). 27th European Symposium on Programming, ESOP 2018. Springer VS. (Lecture Notes in Computer Science (LNCS); Journal number 10801). 2018, 214-241. https://doi.org/10.1007/978-3-319-89884-1_8

Vancouver

Aguirre A, Barthe G, Birkedal L, Bizjak A, Gaboardi M, Garg D. Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. In Ahmed A, editor, 27th European Symposium on Programming, ESOP 2018. Springer VS. 2018. p. 214-241. (Lecture Notes in Computer Science (LNCS); No. 10801). https://doi.org/10.1007/978-3-319-89884-1_8

Author

Aguirre, Alejandro ; Barthe, Gilles ; Birkedal, Lars ; Bizjak, Aleš ; Gaboardi, Marco ; Garg, Deepak. / Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. 27th European Symposium on Programming, ESOP 2018. editor / Amal Ahmed. Springer VS, 2018. pp. 214-241 (Lecture Notes in Computer Science (LNCS); No. 10801).

Bibtex

@inproceedings{48dae92878924ab881849cfbf11dae16,
title = "Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus",
abstract = " 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. ",
keywords = "cs.PL",
author = "Alejandro Aguirre and Gilles Barthe and Lars Birkedal and Ale{\v s} Bizjak and Marco Gaboardi and Deepak Garg",
year = "2018",
month = apr,
day = "18",
doi = "10.1007/978-3-319-89884-1_8",
language = "English",
isbn = "9783319898834",
series = "Lecture Notes in Computer Science (LNCS)",
publisher = "Springer VS",
number = "10801",
pages = "214--241",
editor = "Ahmed, {Amal }",
booktitle = "27th European Symposium on Programming, ESOP 2018",
note = "ETAPS 2018 ; Conference date: 14-04-2018 Through 20-04-2018",
url = "https://www.etaps.org/",

}

RIS

TY - GEN

T1 - Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus

AU - Aguirre, Alejandro

AU - Barthe, Gilles

AU - Birkedal, Lars

AU - Bizjak, Aleš

AU - Gaboardi, Marco

AU - Garg, Deepak

PY - 2018/4/18

Y1 - 2018/4/18

N2 - 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.

AB - 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.

KW - cs.PL

U2 - 10.1007/978-3-319-89884-1_8

DO - 10.1007/978-3-319-89884-1_8

M3 - Article in proceedings

SN - 9783319898834

T3 - Lecture Notes in Computer Science (LNCS)

SP - 214

EP - 241

BT - 27th European Symposium on Programming, ESOP 2018

A2 - Ahmed, Amal

PB - Springer VS

T2 - ETAPS 2018

Y2 - 14 April 2018 through 20 April 2018

ER -