On Probabilistic Applicative Bisimulation and Call-by-Value\n \λ-Calculi (Long Version)

2014/01/15 by Raphaëlle Crubillé, Crubille, Raphaelle, Ugo Dal Lago +1 · 1 citation
Computer Science · #F.1.2 #F.3.1 #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems

paper · pdf · doi:10.48550/arxiv.1401.3766

openalex publication_date 2014/01/15 · openalex created_date 2022/10/02 · openalex updated_date 2026/07/28

Abstract

Probabilistic applicative bisimulation is a recently introduced coinductive\nmethodology for program equivalence in a probabilistic, higher-order, setting.\nIn this paper, the technique is applied to a typed, call-by-value,\nlambda-calculus. Surprisingly, the obtained relation coincides with context\nequivalence, contrary to what happens when call-by-name evaluation is\nconsidered. Even more surprisingly, full-abstraction only holds in a symmetric\nsetting.\n

Cited by

• Contextual Refinement of Higher-Order Concurrent Probabilistic Programs

Related

• The Benefit of Being Non-Lazy in Probabilistic \λ-calculus
• On Coinductive Equivalences for Higher-Order Probabilistic Functional Programs (Long Version)
• A Probabilistic Call-by-Need Lambda-Calculus -- Extended Version
• Lambda Calculus and Probabilistic Computation
• Applicative Bisimulation and Quantum λ-Calculi (Long Version)