The Computational Meaning of Probabilistic Coherence Spaces

Author

Ehrhard, Thomas ; Pagani, Michele ; Tasson, Christine

Author_Institution

Lab. PPS, Univ. Paris Diderot, Paris, France

fYear

2011

fDate

21-24 June 2011

Firstpage

87

Lastpage

96

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 λ-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 λ-calculus.

Keywords

pi calculus; probability; programming language semantics; Scott´s model; denotational semantic interpreting programs; nonnegative real coefficients; power series; probabilistic coherent spaces; untyped λ-calculus; Coherence; Computational modeling; Equations; Indexes; Mathematical model; Probabilistic logic; Semantics; Adequacy Theorem; Coherence Spaces; Denotational Semantics; Linear Logic; Probabilistic Lambda Calculus;

fLanguage

English

Publisher

ieee

Conference_Titel

Logic in Computer Science (LICS), 2011 26th Annual IEEE Symposium on

Conference_Location

Toronto, ON

ISSN

1043-6871

Print_ISBN

978-1-4577-0451-2

Electronic_ISBN

1043-6871

Type

conf

DOI

10.1109/LICS.2011.29

Filename

5970206