Date(s) : 28/02/2019
11 h 00 min - 12 h 30 min
In order to model higher-order probabilistic computation, a natural approach is to take the lambda calculus as a paradigm, and to enrich it with an operator which models probabilistic choice. The resulting calculus is however not confluent; such an issue is typically handled in the literature by fixing a deterministic reduction strategy.
Following [Plotkin75], we wish to preserve the key distinction between a calculus and a programming language. The former defines terms and reduction rules, and satisfy confluence, the latter is specified by a deterministic strategy (an abstract machine). Standardization is what relates the two: the programming language implements the standard strategy associated to the calculus. We propose two probabilistic lambda calculi, based respectively on the call-by-value and call-by-name parameter passing mechanism. The common root of the two calculi is a further calculus based on Linear Logic, which allows us to develop a unified, modular approach.
(joint work with Simona Ronchi Della Rocca)