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 M to the continuation λ v. 0 yields the expected cost of M. 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.

Avanzini M., Barthe G., Dal Lago U. (2021). On continuation-passing transformations and expected cost analysis. PROCEEDINGS OF ACM ON PROGRAMMING LANGUAGES, 5(ICFP), 1-30 [10.1145/3473592].

On continuation-passing transformations and expected cost analysis

Dal Lago U.
2021

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 M to the continuation λ v. 0 yields the expected cost of M. 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.
2021
Avanzini M., Barthe G., Dal Lago U. (2021). On continuation-passing transformations and expected cost analysis. PROCEEDINGS OF ACM ON PROGRAMMING LANGUAGES, 5(ICFP), 1-30 [10.1145/3473592].
Avanzini M.; Barthe G.; Dal Lago U.
File in questo prodotto:
File Dimensione Formato  
icfp2021.pdf

accesso aperto

Tipo: Versione (PDF) editoriale
Licenza: Licenza per Accesso Aperto. Creative Commons Attribuzione (CCBY)
Dimensione 414.88 kB
Formato Adobe PDF
414.88 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/834261
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 10
  • ???jsp.display-item.citation.isi??? 5
social impact