ICFP 2021
Sun 22 - Sat 28 August 2021
Wed 25 Aug 2021 16:00 - 16:15 at ICFP Talks - Session 5
Thu 26 Aug 2021 04:00 - 04:15 at ICFP Talks - Session 5

We define a continuation-passing style (CPS) translation for a typed $\lambda$-calculus with probabilistic choice, unbounded recursion, and a tick operator — for modeling cost. The target language is a (non-probabilistic) $\lambda$-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 $\lambda 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 \textsf{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 $\lambda$-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.

Wed 25 Aug

Displayed time zone: Seoul change

16:00 - 17:30
16:00
15m
Talk
On Continuation-Passing Transformations and Expected Cost Analysis
Research Papers
Martin Avanzini Inria, Gilles Barthe MPI-SP; IMDEA Software Institute, Ugo Dal Lago University of Bologna, Italy / Inria, France
DOI Media Attached
16:15
15m
Talk
Steel: Proof-Oriented Programming in a Dependently Typed Concurrent Separation Logic
Research Papers
Aymeric Fromherz Carnegie Mellon University, Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research, Sydney Gibson Carnegie Mellon University, Guido Martínez CIFASIS-CONICET, Argentina, Denis Merigoux INRIA, Tahina Ramananandro Microsoft Research
DOI Media Attached
16:30
15m
Talk
Automatic Amortized Resource Analysis with the Quantum Physicist’s Method
Research Papers
David M. Kahn Carnegie Mellon University, Jan Hoffmann Carnegie Mellon University
DOI Media Attached
16:45
15m
Talk
Theorems for Free from Separation Logic SpecificationsDistinguished Paper
Research Papers
Lars Birkedal Aarhus University, Thomas Dinsdale-Young Concordium, Armaël Guéneau Aarhus University, Guilhem Jaber University of Nantes, Kasper Svendsen Uber, Nikos Tzevelekos Queen Mary University of London
DOI Pre-print Media Attached
17:00
15m
Talk
Reasoning about the Garden of Forking Paths
Research Papers
Yao Li University of Pennsylvania, Li-yao Xia University of Pennsylvania, Stephanie Weirich University of Pennsylvania
DOI Pre-print Media Attached
17:15
15m
Talk
Formal Verification of a Concurrent Bounded Queue in a Weak Memory Model
Research Papers
Glen Mével Inria; University of Paris-Saclay; CNRS; ENS Paris-Saclay; LMF, Jacques-Henri Jourdan Universersité Paris Saclay, CNRS, LRI
DOI Media Attached

Thu 26 Aug

Displayed time zone: Seoul change

04:00 - 05:30
Session 5Research Papers at ICFP Talks
04:00
15m
Talk
On Continuation-Passing Transformations and Expected Cost Analysis
Research Papers
Martin Avanzini Inria, Gilles Barthe MPI-SP; IMDEA Software Institute, Ugo Dal Lago University of Bologna, Italy / Inria, France
DOI Media Attached
04:15
15m
Talk
Steel: Proof-Oriented Programming in a Dependently Typed Concurrent Separation Logic
Research Papers
Aymeric Fromherz Carnegie Mellon University, Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research, Sydney Gibson Carnegie Mellon University, Guido Martínez CIFASIS-CONICET, Argentina, Denis Merigoux INRIA, Tahina Ramananandro Microsoft Research
DOI Media Attached
04:30
15m
Talk
Automatic Amortized Resource Analysis with the Quantum Physicist’s Method
Research Papers
David M. Kahn Carnegie Mellon University, Jan Hoffmann Carnegie Mellon University
DOI Media Attached
04:45
15m
Talk
Theorems for Free from Separation Logic SpecificationsDistinguished Paper
Research Papers
Lars Birkedal Aarhus University, Thomas Dinsdale-Young Concordium, Armaël Guéneau Aarhus University, Guilhem Jaber University of Nantes, Kasper Svendsen Uber, Nikos Tzevelekos Queen Mary University of London
DOI Pre-print Media Attached
05:00
15m
Talk
Reasoning about the Garden of Forking Paths
Research Papers
Yao Li University of Pennsylvania, Li-yao Xia University of Pennsylvania, Stephanie Weirich University of Pennsylvania
DOI Pre-print Media Attached
05:15
15m
Talk
Formal Verification of a Concurrent Bounded Queue in a Weak Memory Model
Research Papers
Glen Mével Inria; University of Paris-Saclay; CNRS; ENS Paris-Saclay; LMF, Jacques-Henri Jourdan Universersité Paris Saclay, CNRS, LRI
DOI Media Attached