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

Multicore OCaml extends OCaml with support for shared-memory concurrency. It is equipped with a weak memory model, for which an operational semantics has been published. This begs the question: what reasoning rules can one rely upon while writing or verifying Multicore OCaml code? To answer it, we instantiate Iris, a modern descendant of Concurrent Separation Logic, for Multicore OCaml. This yields a low-level program logic whose reasoning rules expose the details of the memory model. On top of it, we build a higher-level logic, Cosmo, which trades off some expressive power in return for a simple set of reasoning rules that allow accessing nonatomic locations in a data-race-free manner, exploiting the sequentially-consistent behavior of atomic locations, and exploiting the release/acquire behavior of atomic locations. Cosmo allows both low-level reasoning, where the details of the Multicore OCaml memory model are apparent, and high-level reasoning, which is independent of this memory model. We illustrate this claim via a number of case studies: we verify several implementations of locks with respect to a classic, memory-model-independent specification. Thus, a coarse-grained application that uses locks as the sole means of synchronization can be verified in the Concurrent-Separation-Logic fragment of Cosmo, without any knowledge of the weak memory model.

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 Weirich University 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 Knoth University of California at San Diego, USA, Di Wang Carnegie Mellon University, Adam Reynolds University of California, San Diego, Nadia Polikarpova University of California, San Diego, Jan Hoffmann Carnegie Mellon University
DOI Media Attached
15:00
15m
Talk
Cosmo: A Concurrent Separation Logic for Multicore OCaml
ICFP Program
Glen Mével Inria, Université Paris-Saclay, CNRS, Laboratoire de recherche en informatique, Jacques-Henri Jourdan Universersité Paris Saclay, CNRS, LRI, François Pottier Inria, France
DOI Media Attached
15:15
15m
Talk
Composing and Decomposing Op-Based CRDTs with Semidirect Products
ICFP Program
Matthew Weidner Carnegie Mellon University, Christopher Meiklejohn Carnegie Mellon University, Heather Miller Carnegie Mellon University
DOI Media Attached
15:30
15m
Talk
A Quick Look at ImpredicativityDistinguished Paper
ICFP Program
Alejandro Serrano 47 Degrees, Spain, Jurriaan Hage Utrecht University, Netherlands, Simon Peyton Jones Microsoft, UK, Dimitrios Vytiniotis DeepMind
DOI Pre-print Media Attached
15:45
15m
Talk
A Unified View of Modalities in Type Systems
ICFP Program
Andreas Abel Gothenburg University, Jean-Philippe Bernardy University of Gothenburg, Sweden
DOI Media Attached
16:00
15m
Talk
Lower Your Guards: A Compositional Pattern-Match Coverage Checker
ICFP Program
Sebastian Graf Karlsruhe Institute of Technology, Simon Peyton Jones Microsoft, UK, Ryan Scott Galois, Inc.
Link to publication DOI Media Attached
16:15
15m
Talk
Signature restriction for polymorphic algebraic effects
ICFP Program
Taro Sekiyama National Institute of Informatics, Takeshi Tsukada Chiba University, Japan, Atsushi Igarashi Kyoto University, Japan
DOI Media Attached

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 Weirich University 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 Knoth University of California at San Diego, USA, Di Wang Carnegie Mellon University, Adam Reynolds University of California, San Diego, Nadia Polikarpova University of California, San Diego, Jan Hoffmann Carnegie Mellon University
DOI Media Attached
03:00
15m
Talk
Cosmo: A Concurrent Separation Logic for Multicore OCaml
ICFP Program
Glen Mével Inria, Université Paris-Saclay, CNRS, Laboratoire de recherche en informatique, Jacques-Henri Jourdan Universersité Paris Saclay, CNRS, LRI, François Pottier Inria, France
DOI Media Attached
03:15
15m
Talk
Composing and Decomposing Op-Based CRDTs with Semidirect Products
ICFP Program
Matthew Weidner Carnegie Mellon University, Christopher Meiklejohn Carnegie Mellon University, Heather Miller Carnegie Mellon University
DOI Media Attached
03:30
15m
Talk
A Quick Look at ImpredicativityDistinguished Paper
ICFP Program
Alejandro Serrano 47 Degrees, Spain, Jurriaan Hage Utrecht University, Netherlands, Simon Peyton Jones Microsoft, UK, Dimitrios Vytiniotis DeepMind
DOI Pre-print Media Attached
03:45
15m
Talk
A Unified View of Modalities in Type Systems
ICFP Program
Andreas Abel Gothenburg University, Jean-Philippe Bernardy University of Gothenburg, Sweden
DOI Media Attached
04:00
15m
Talk
Lower Your Guards: A Compositional Pattern-Match Coverage Checker
ICFP Program
Sebastian Graf Karlsruhe Institute of Technology, Simon Peyton Jones Microsoft, UK, Ryan Scott Galois, Inc.
Link to publication DOI Media Attached
04:15
15m
Talk
Signature restriction for polymorphic algebraic effects
ICFP Program
Taro Sekiyama National Institute of Informatics, Takeshi Tsukada Chiba University, Japan, Atsushi Igarashi Kyoto University, Japan
DOI Media Attached