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

We present a novel method for working with the physicist's method of amortized resource analysis, which we call the quantum physicist's method. These principles allow for more precise analyses of resources that are not monotonically consumed, like stack. This method takes its name from its two major features, worldviews and resource tunneling, which behave analogously to quantum superposition and quantum tunneling. We use the quantum physicist's method to extend the Automatic Amortized Resource Analysis (AARA) type system, enabling the derivation of resource bounds based on tree depth. In doing so, we also introduce remainder contexts, which aid bookkeeping in linear type systems. We then evaluate this new type system's performance by bounding stack use of functions in the Set module of OCaml's standard library. Compared to state-of-the-art implementations of AARA, our new system derives tighter bounds with only moderate overhead.

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