Article

The Computational Meaning of Probabilistic Coherence Spaces

Authors:

Thomas Ehrhard,

Michele Pagani,

Christine TassonAuthors Info & Claims

LICS '11: Proceedings of the 2011 IEEE 26th Annual Symposium on Logic in Computer Science

Pages 87 - 96

https://doi.org/10.1109/LICS.2011.29

Published: 21 June 2011 Publication History

Abstract

We study the probabilistic coherent spaces--a denotational semantics interpreting programs by power series with non negative real coefficients. We prove that this semantics is adequate for a probabilistic extension of the untyped $\lambda$-calculus: the probability that a term reduces to ahead normal form is equal to its denotation computed on a suitable set of values. The result gives, in a probabilistic setting, a quantitative refinement to the adequacy of Scott's model for untyped $\lambda$-calculus.

Cited By

View all

Curzi GPagani MHermanns HZhang LKobayashi NMiller D(2020)The Benefit of Being Non-Lazy in Probabilistic λ-calculusProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3373718.3394806(327-340)Online publication date: 8-Jul-2020
https://dl.acm.org/doi/10.1145/3373718.3394806
Ehrhard THermanns HZhang LKobayashi NMiller D(2020)Cones as a model of intuitionistic linear logicProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3373718.3394758(370-383)Online publication date: 8-Jul-2020
https://dl.acm.org/doi/10.1145/3373718.3394758
Faggian CRocca SBouyer P(2019)Lambda calculus and probabilistic computationProceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3470152.3470186(1-13)Online publication date: 24-Jun-2019
https://dl.acm.org/doi/10.5555/3470152.3470186
Show More Cited By

The Computational Meaning of Probabilistic Coherence Spaces
1. Theory of computation
  1. Semantics and reasoning

Recommendations

Probabilistic coherence spaces as a model of higher-order probabilistic computation

We study a probabilistic version of coherence spaces and show that these objects provide a model of linear logic. We build a model of the pure lambda-calculus in this setting and show how to interpret a probabilistic version of the functional language ...
The Bang Calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value
PPDP '16: Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming

We introduce and study the Bang Calculus, an untyped functional calculus in which the promotion operation of Linear Logic is made explicit and where application is a bilinear operation. This calculus, which can be understood as an untyped version of ...
Call-by-push-value in Coq: operational, equational, and denotational theory
CPP 2019: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs

Call-by-push-value (CBPV) is an idealised calculus for functional and imperative programming, introduced as a subsuming paradigm for both call-by-value (CBV) and call-by-name (CBN). We formalise weak and strong operational semantics for (effect-free) ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

LICS '11: Proceedings of the 2011 IEEE 26th Annual Symposium on Logic in Computer Science

June 2011

379 pages

ISBN:9780769544120

Publisher

IEEE Computer Society

United States

Publication History

Published: 21 June 2011

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Curzi GPagani MHermanns HZhang LKobayashi NMiller D(2020)The Benefit of Being Non-Lazy in Probabilistic λ-calculusProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3373718.3394806(327-340)Online publication date: 8-Jul-2020
https://dl.acm.org/doi/10.1145/3373718.3394806
Ehrhard THermanns HZhang LKobayashi NMiller D(2020)Cones as a model of intuitionistic linear logicProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3373718.3394758(370-383)Online publication date: 8-Jul-2020
https://dl.acm.org/doi/10.1145/3373718.3394758
Faggian CRocca SBouyer P(2019)Lambda calculus and probabilistic computationProceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3470152.3470186(1-13)Online publication date: 24-Jun-2019
https://dl.acm.org/doi/10.5555/3470152.3470186
Leventis T(2018)Probabilistic Böhm Trees and Probabilistic SeparationProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3209108.3209126(649-658)Online publication date: 9-Jul-2018
https://dl.acm.org/doi/10.1145/3209108.3209126
Ehrhard TPagani MTasson C(2018)Full Abstraction for Probabilistic PCFJournal of the ACM10.1145/316454065:4(1-44)Online publication date: 26-Apr-2018
https://dl.acm.org/doi/10.1145/3164540
Ehrhard TPagani MTasson C(2017)Measurable cones and stable, measurable functions: a model for probabilistic higher-order programmingProceedings of the ACM on Programming Languages10.1145/31581472:POPL(1-28)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158147
Dal Lago USangiorgi DAlberti M(2014)On coinductive equivalences for higher-order probabilistic functional programsACM SIGPLAN Notices10.1145/2578855.253587249:1(297-308)Online publication date: 8-Jan-2014
https://dl.acm.org/doi/10.1145/2578855.2535872
Dal Lago USangiorgi DAlberti MJagannathan SSewell P(2014)On coinductive equivalences for higher-order probabilistic functional programsProceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages10.1145/2535838.2535872(297-308)Online publication date: 11-Jan-2014
https://dl.acm.org/doi/10.1145/2535838.2535872
Laird JManzonetto GMcCusker GPagani M(2013)Weighted Relational Models of Typed Lambda-CalculiProceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS.2013.36(301-310)Online publication date: 25-Jun-2013
https://dl.acm.org/doi/10.1109/LICS.2013.36

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract

Cited By

Recommendations

Probabilistic coherence spaces as a model of higher-order probabilistic computation

The Bang Calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value

Call-by-push-value in Coq: operational, equational, and denotational theory

Comments

Information

Published In

Publisher

Publication History

Author Tags

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations