Write a Blog >>
ICFP 2020
Thu 20 - Fri 28 August 2020
Tue 25 Aug 2020 14:45 - 15:00 at ICFP NY 4 - New York 4 Chair(s): Stephanie Weirich
Wed 26 Aug 2020 02:45 - 03:00 at ICFP Asia 4 - Asia 4 Chair(s): Stephanie Weirich

This article presents \emph{liquid resource types}, a technique for automatically verifying the resource consumption of functional programs. Existing resource analysis techniques trade automation for flexibility – automated techniques are restricted to relatively constrained families of resource bounds, while more expressive proof techniques admitting value-dependent bounds rely on handwritten proofs. Liquid resource types combine the best of these approaches, using logical refinements to automatically prove precise bounds on a program’s resource consumption. The type system augments refinement types with potential annotations to conduct an amortized resource analysis. Importantly, users can annotate data structure declarations to indicate how potential is allocated within the type, allowing the system to express bounds with polynomials and exponentials, as well as more precise expressions depending on program values. We prove the soundness of the type system, provide a library of flexible and reusable data structures for conducting resource analysis, and use our prototype implementation to automatically verify resource bounds that previously required a manual proof.

Conference Day
Tue 25 Aug

Displayed time zone: Eastern Time (US & Canada) change

14:30 - 16:30
New York 4ICFP Program at ICFP NY 4
Chair(s): Stephanie WeirichUniversity of Pennsylvania

Public livestreams: YouTube, Bilibili (China)

14:30
15m
Talk
The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy (Functional Pearl)
ICFP Program
DOI Pre-print Media Attached
14:45
15m
Talk
Liquid Resource Types
ICFP Program
Tristan KnothUniversity of California at San Diego, USA, Di WangCarnegie Mellon University, Adam ReynoldsUniversity of California, San Diego, Nadia PolikarpovaUniversity of California, San Diego, Jan HoffmannCarnegie Mellon University
DOI Media Attached
15:00
15m
Talk
Cosmo: A Concurrent Separation Logic for Multicore OCaml
ICFP Program
Glen MévelInria, Université Paris-Saclay, CNRS, Laboratoire de recherche en informatique, Jacques-Henri JourdanUniversersité Paris Saclay, CNRS, LRI, François PottierInria, France
DOI Media Attached
15:15
15m
Talk
Composing and Decomposing Op-Based CRDTs with Semidirect Products
ICFP Program
Matthew WeidnerCarnegie Mellon University, Christopher MeiklejohnCarnegie Mellon University, Heather MillerCarnegie Mellon University
DOI Media Attached
15:30
15m
Talk
A Quick Look at ImpredicativityDistinguished Paper
ICFP Program
Alejandro Serrano47 Degrees, Spain, Jurriaan HageUtrecht University, Netherlands, Simon Peyton JonesMicrosoft, UK, Dimitrios VytiniotisDeepMind
DOI Pre-print Media Attached
15:45
15m
Talk
A Unified View of Modalities in Type Systems
ICFP Program
Andreas AbelGothenburg University, Jean-Philippe BernardyUniversity of Gothenburg, Sweden
DOI Media Attached
16:00
15m
Talk
Lower Your Guards: A Compositional Pattern-Match Coverage Checker
ICFP Program
Sebastian GrafKarlsruhe Institute of Technology, Simon Peyton JonesMicrosoft, UK, Ryan ScottGalois, Inc.
Link to publication DOI Media Attached
16:15
15m
Talk
Signature restriction for polymorphic algebraic effects
ICFP Program
Taro SekiyamaNational Institute of Informatics, Takeshi TsukadaChiba University, Japan, Atsushi IgarashiKyoto University, Japan
DOI Media Attached

Conference Day
Wed 26 Aug

Displayed time zone: Eastern Time (US & Canada) change

02:30 - 04:30
Asia 4ICFP Program at ICFP Asia 4
Chair(s): Stephanie WeirichUniversity of Pennsylvania

Public livestreams: YouTube, Bilibili (China)

02:30
15m
Talk
The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy (Functional Pearl)
ICFP Program
DOI Pre-print Media Attached
02:45
15m
Talk
Liquid Resource Types
ICFP Program
Tristan KnothUniversity of California at San Diego, USA, Di WangCarnegie Mellon University, Adam ReynoldsUniversity of California, San Diego, Nadia PolikarpovaUniversity of California, San Diego, Jan HoffmannCarnegie Mellon University
DOI Media Attached
03:00
15m
Talk
Cosmo: A Concurrent Separation Logic for Multicore OCaml
ICFP Program
Glen MévelInria, Université Paris-Saclay, CNRS, Laboratoire de recherche en informatique, Jacques-Henri JourdanUniversersité Paris Saclay, CNRS, LRI, François PottierInria, France
DOI Media Attached
03:15
15m
Talk
Composing and Decomposing Op-Based CRDTs with Semidirect Products
ICFP Program
Matthew WeidnerCarnegie Mellon University, Christopher MeiklejohnCarnegie Mellon University, Heather MillerCarnegie Mellon University
DOI Media Attached
03:30
15m
Talk
A Quick Look at ImpredicativityDistinguished Paper
ICFP Program
Alejandro Serrano47 Degrees, Spain, Jurriaan HageUtrecht University, Netherlands, Simon Peyton JonesMicrosoft, UK, Dimitrios VytiniotisDeepMind
DOI Pre-print Media Attached
03:45
15m
Talk
A Unified View of Modalities in Type Systems
ICFP Program
Andreas AbelGothenburg University, Jean-Philippe BernardyUniversity of Gothenburg, Sweden
DOI Media Attached
04:00
15m
Talk
Lower Your Guards: A Compositional Pattern-Match Coverage Checker
ICFP Program
Sebastian GrafKarlsruhe Institute of Technology, Simon Peyton JonesMicrosoft, UK, Ryan ScottGalois, Inc.
Link to publication DOI Media Attached
04:15
15m
Talk
Signature restriction for polymorphic algebraic effects
ICFP Program
Taro SekiyamaNational Institute of Informatics, Takeshi TsukadaChiba University, Japan, Atsushi IgarashiKyoto University, Japan
DOI Media Attached