On Probabilistic Applicative Bisimulation and Call-by-Value λ-Calculi (Long Version)
classification
💻 cs.LO
keywords
probabilisticapplicativebisimulationcall-by-valueequivalencesettingsurprisinglyapplied
pith:SLTFXVGP Add to your LaTeX paper
What is a Pith Number?\usepackage{pith}
\pithnumber{SLTFXVGP}
Prints a linked pith:SLTFXVGP badge after your title and writes the identifier into PDF metadata. Compiles on arXiv with no extra files. Learn more
read the original abstract
Probabilistic applicative bisimulation is a recently introduced coinductive methodology for program equivalence in a probabilistic, higher-order, setting. In this paper, the technique is applied to a typed, call-by-value, lambda-calculus. Surprisingly, the obtained relation coincides with context equivalence, contrary to what happens when call-by-name evaluation is considered. Even more surprisingly, full-abstraction only holds in a symmetric setting.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.