On bisimilarity in lambda calculi with continuous probabilistic choice

DOI10.1016/J.ENTCS.2019.09.007OpenAlexW2995436578WikidataQ113317356 ScholiaQ113317356MaRDI QIDQ2133169FDOQ2133169

Authors: Ugo Dal Lago, Francesco Gavazzo 

Publication date: 29 April 2022

Full work available at URL: https://doi.org/10.1016/j.entcs.2019.09.007

Recommendations

• On probabilistic applicative bisimulation and call-by-value \(\lambda \)-calculi
• On coinductive equivalences for higher-order probabilistic functional programs
• On applicative similarity, sequentiality, and full abstraction
• Applicative bisimulation and quantum \(\lambda\)-calculi
• The Benefit of Being Non-Lazy in Probabilistic λ-calculus

zbMATH Keywords

\(\lambda\)-calculuscontinuous distributionsprobabilistic computation

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Cites Work

• Modelling environments in call-by-value programming languages.
• Nondeterministic extensions of untyped \(\lambda\)-calculus
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Fixpoint semantics and simulation
• Proving congruence of bisimulation in functional programming languages
• Title not available (Why is that?)
• Title not available (Why is that?)
• Relational algebras
• A user's guide to measure theoretic probability
• Similarity quotients as final coalgebras
• Simulations in coalgebra
• Stochastic lambda calculus and monads of probability distributions
• Title not available (Why is that?)
• Equivalence in functional languages with effects
• Title not available (Why is that?)
• Title not available (Why is that?)
• Logical relations for monadic types
• Distance makes the types grow stronger: a calculus for differential privacy
• Domain theory, testing and simulation for labelled Markov processes
• The lazy lambda calculus in a concurrency scenario
• A probabilistic language based upon sampling functions
• Relational reasoning about contexts
• Typed Normal Form Bisimulation
• Infinitary Howe's method
• Behavioural equivalence via modalities for algebraic effects
• Contextual equivalence for probabilistic programs with continuous random variables and scoring
• Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints
• Approximate relational Hoare logic for continuous random samplings
• A semantic account of metric preservation
• Step-indexed logical relations for probability
• Effectful applicative bisimilarity: monads, relators, and Howe's method
• On coinductive equivalences for higher-order probabilistic functional programs
• On probabilistic applicative bisimulation and call-by-value \(\lambda \)-calculi
• Howe's method for higher-order languages
• A lambda-calculus foundation for universal probabilistic programming
• Commutative semantics for probabilistic programming
• Codensity lifting of monads and its dual
• Quantitative Behavioural Reasoning for Higher-order Effectful Programs
• Probabilistic bisimulation

Cited In (2)

• The Benefit of Being Non-Lazy in Probabilistic λ-calculus
• A fibrational tale of operational logical relations: pure, effectful and differential

This page was built for publication: On bisimilarity in lambda calculi with continuous probabilistic choice

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