Skip to Main content Skip to Navigation
Journal articles

On continuation-passing transformations and expected cost analysis

Martin Avanzini 1 Gilles Barthe 2 Ugo Dal Lago 1 
1 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : We define a continuation-passing style (CPS) translation for a typed-calculus with probabilistic choice, unbounded recursion, and a tick operator-for modeling cost. The target language is a (non-probabilistic)-calculus, enriched with a type of extended positive reals and a fixpoint operator. We then show that applying the CPS transform of an expression to the continuation .0 yields the expected cost of. We also introduce a formal system for higher-order logic, called EHOL, prove it sound, and show it can derive tight upper bounds on the expected cost of classic examples, including Coupon Collector and Random Walk. Moreover, we relate our translation to Kaminski et al. 's ert-calculus, showing that the latter can be recovered by applying our CPS translation to (a generalization of) the classic embedding of imperative programs into-calculus. Finally, we prove that the CPS transform of an expression can also be used to compute pre-expectations and to reason about almost sure termination.
Document type :
Journal articles
Complete list of metadata
Contributor : Martin Avanzini Connect in order to contact the contributor
Submitted on : Wednesday, September 8, 2021 - 4:46:22 PM
Last modification on : Friday, July 8, 2022 - 10:04:28 AM
Long-term archiving on: : Friday, December 10, 2021 - 9:55:35 AM


Files produced by the author(s)




Martin Avanzini, Gilles Barthe, Ugo Dal Lago. On continuation-passing transformations and expected cost analysis. Proceedings of the ACM on Programming Languages, ACM, 2021, 5 (ICFP), pp.1 - 30. ⟨10.1145/3473592⟩. ⟨hal-03338493⟩



Record views


Files downloads