@inbook{10.1145/3531130.3533361,
    Abstract = {We show that an intuitionistic version of counting propositional logic corresponds, in the sense of Curry and Howard, to an expressive type system for the probabilistic event {$\lambda$}-calculus, a vehicle calculus in which both call-by-name and call-by-value evaluation of discrete randomized functional programs can be simulated. In this context, proofs (respectively, types) do not guarantee that validity (respectively, termination) holds, but reveal the underlying probability. We finally show how to obtain a system precisely capturing the probabilistic behavior of {$\lambda$}-terms, by endowing the type system with an intersection operator.},
    Address = {New York, NY, USA},
    Author = {Antonelli, Melissa and Dal Lago, Ugo and Pistone, Paolo},
    BookTitle = {Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science},
    File = {Curry and Howard Meet Borel - 3531130.3533361 - a.pdf},
    ISBN = {9781450393515},
    Publisher = {Association for Computing Machinery},
    Title = {Curry and Howard Meet Borel},
    URL = {https://doi.org/10.1145/3531130.3533361},
    Year = {2022},
    articleno = {45},
    bdsk-url-1 = {https://doi.org/10.1145/3531130.3533361},
    date-added = {2022-11-02 07:05:40 +0100},
    date-modified = {2022-11-02 07:05:40 +0100},
    numpages = {13},
    doi = {10.1145/3531130.3533361}
}

@inbook{10.1145/3531130.3533361, Abstract = {We show that an intuitionistic version of counting propositional logic corresponds, in the sense of Curry and Howard, to an expressive type system for the probabilistic event {$\lambda$}-calculus, a vehicle calculus in which both call-by-name and call-by-value evaluation of discrete randomized functional programs can be simulated. In this context, proofs (respectively, types) do not guarantee that validity (respectively, termination) holds, but reveal the underlying probability. We finally show how to obtain a system precisely capturing the probabilistic behavior of {$\lambda$}-terms, by endowing the type system with an intersection operator.}, Address = {New York, NY, USA}, Author = {Antonelli, Melissa and Dal Lago, Ugo and Pistone, Paolo}, BookTitle = {Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science}, File = {Curry and Howard Meet Borel - 3531130.3533361 - a.pdf}, ISBN = {9781450393515}, Publisher = {Association for Computing Machinery}, Title = {Curry and Howard Meet Borel}, URL = {https://doi.org/10.1145/3531130.3533361}, Year = {2022}, articleno = {45}, bdsk-url-1 = {https://doi.org/10.1145/3531130.3533361}, date-added = {2022-11-02 07:05:40 +0100}, date-modified = {2022-11-02 07:05:40 +0100}, numpages = {13}, doi = {10.1145/3531130.3533361} }