Step-indexed logical relations for probability

DOI10.1007/978-3-662-46678-0_18MaRDI QIDQ2949445zbMATH OpenOpenAlexFDO

Authors Aleš Bizjak, Lars Birkedal

Publication date 1 October 2015

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1501.02623

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Abstract: It is well-known that constructing models of higher-order probabilistic programming languages is challenging. We show how to construct step-indexed logical relations for a probabilistic extension of a higher-order programming language with impredicative polymorphism and recursive types. We show that the resulting logical relation is sound and complete with respect to the contextual preorder and, moreover, that it is convenient for reasoning about concrete program equivalences. Finally, we extend the language with dynamically allocated first-order references and show how to extend the logical relation to this language. We show that the resulting relation remains useful for reasoning about examples involving both state and probabilistic choice.

Recommendations

• Step-indexed relational reasoning for countable nondeterminism
• Step-indexed relational reasoning for countable nondeterminism
• Transfinite step-indexing: decoupling concrete and logical steps
• A relational modal logic for higher-order stateful ADTs
• Programming Languages and Systems

Cited in

(17)

• Effectful applicative similarity for call-by-name lambda calculi
• On bisimilarity in lambda calculi with continuous probabilistic choice
• Relational reasoning for Markov chains in a probabilistic guarded lambda calculus
• Transfinite step-indexing: decoupling concrete and logical steps
• Step-indexed relational reasoning for countable nondeterminism
• Step-indexed relational reasoning for countable nondeterminism
• Metric reasoning about -terms: the general case
• Contextual equivalence for probabilistic programs with continuous random variables and scoring
• The beta-Bernoulli process and algebraic effects
• On the versatility of open logical relations. Continuity, automatic differentiation, and a containment theorem
• A relational modal logic for higher-order stateful ADTs
• Programming Languages and Systems
• Program equivalence in a typed probabilistic call-by-need functional language
• A fibrational tale of operational logical relations: pure, effectful and differential
• Logical predicates in higher-order mathematical operational semantics
• A model of stochastic memoization and name generation in probabilistic programming: categorical semantics via monads on presheaf categories
• Bialgebraic reasoning on higher-order program equivalence

This page was built for publication: Step-indexed logical relations for probability

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2949445)