xThe data center, from which the conference websites are hosted, is currently experiencing power issues. Our colleagues are working hard to resolve the issue and keep downtime to a minimum.
ICFP 2021
Sun 22 - Sat 28 August 2021
Wed 25 Aug 2021 17:15 - 17:30 at ICFP Talks - Session 5
Thu 26 Aug 2021 05:15 - 05:30 at ICFP Talks - Session 5

We use Cosmo, a modern concurrent separation logic, to formally specify and verify an implementation of a multiple-producer multiple-consumer concurrent queue in the setting of the Multicore OCaml weak memory model. We view this result as a demonstration and experimental verification of the manner in which Cosmo allows modular and formal reasoning about advanced concurrent data structures. In particular, we show how the joint use of logically atomic triples and of Cosmo's views makes it possible to describe precisely in the specification the interaction between the queue library and the weak memory model.

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