Write a Blog >>
ICFP 2020
Thu 20 - Fri 28 August 2020
Mon 24 Aug 2020 15:15 - 15:30 at ICFP NY 2 - New York 2 Chair(s): Alan Jeffrey
Tue 25 Aug 2020 03:15 - 03:30 at ICFP Asia 2 - Asia 2 Chair(s): Alan Jeffrey

Functional programming languages are particularly well-suited for building automated reasoning systems, since (among other reasons) a logical term is well modeled by an inductive type, traversing a term can be implemented generically as a higher-order combinator, and backtracking is dramatically simplified by persistent datastructures. However, existing \emph{pure} functional programming languages all suffer a major limitation in these domains: traversing a term requires time proportional to the tree size of the term as opposed to its graph size. This limitation would be particularly devastating when building automation for interactive theorem provers such as Lean and Coq, for which the exponential blowup of term-tree sizes has proved to be both common and difficult to prevent. All that is needed to recover the optimal scaling is the ability to perform simple operations on the memory addresses of terms, and yet allowing these operations to be used freely would clearly violate the basic premise of referential transparency. We show how to use dependent types to seal the necessary pointer-address manipulations behind pure functional interfaces while requiring only a negligible amount of additional trust. We have implemented our approach for the upcoming version (v4) of Lean, and our approach could be adopted by other languages based on dependent type theory as well.

Mon 24 Aug

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

14:30 - 16:30
New York 2ICFP Program at ICFP NY 2
Chair(s): Alan Jeffrey Mozilla Research

Public livestreams: YouTube, Bilibili (China)

14:30
15m
Talk
Achieving High-Performance the Functional Way - A Functional Pearl on Expressing High-Performance Optimizations as Rewrite Strategies
ICFP Program
Bastian Hagedorn University of Münster, Germany, Johannes Lenfers University of Münster, Thomas Koehler University of Glasgow, United Kingdom, Xueying Qin University of Glasgow, United Kingdom, Sergei Gorlatch University of Münster, Germany, Michel Steuwer The University of Edinburgh
DOI Media Attached
14:45
15m
Talk
Staged Selective Parser Combinators
ICFP Program
Jamie Willis Imperial College London, Nicolas Wu Imperial College London, UK, Matthew Pickering University of Bristol, UK
DOI Media Attached
15:00
15m
Talk
Kindly Bent to Free Us
ICFP Program
Gabriel Radanne Inria, Hannes Saffrich University of Freiburg, Peter Thiemann University of Freiburg, Germany
DOI Pre-print Media Attached File Attached
15:15
15m
Talk
Sealing Pointer-Based Optimizations Behind Pure Functions
ICFP Program
Daniel Selsam Microsoft Research, Simon Hudon Carnegie Mellon University, Leonardo de Moura Microsoft Research, n.n.
DOI Media Attached
15:30
15m
Talk
Effects for Efficiency: Asymptotic Speedup with First-Class Control
ICFP Program
Daniel Hillerström The University of Edinburgh, Sam Lindley Heriot-Watt University, UK / The University of Edinburgh, UK, John Longley The University of Edinburgh
DOI Media Attached
15:45
15m
Talk
Computation Focusing
ICFP Program
Nick Rioux University of Pennsylvania, Steve Zdancewic University of Pennsylvania
DOI Media Attached
16:00
15m
Talk
Retrofitting Parallelism onto OCamlDistinguished Paper
ICFP Program
KC Sivaramakrishnan IIT Madras, Stephen Dolan University of Cambridge, UK, Leo White Jane Street, Sadiq Jaffer Opsian and OCaml Labs, Tom Kelly OCaml Labs, Anmol Sahoo IIT Madras, Sudha Parimala IIT Madras, Atul Dhiman IIT Madras, Anil Madhavapeddy OCaml Labs
DOI Media Attached
16:15
15m
Talk
Liquid Information Flow ControlDistinguished Paper
ICFP Program
Nadia Polikarpova University of California, San Diego, Deian Stefan University of California at San Diego, USA, Jean Yang Carnegie Mellon University, Shachar Itzhaky Technion, Israel, Travis Hance Carnegie Mellon University, Armando Solar-Lezama Massachusetts Institute of Technology, USA
DOI Media Attached

Tue 25 Aug

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

02:30 - 04:30
Asia 2ICFP Program at ICFP Asia 2
Chair(s): Alan Jeffrey Mozilla Research

Public livestreams: YouTube, Bilibili (China)

02:30
15m
Talk
Achieving High-Performance the Functional Way - A Functional Pearl on Expressing High-Performance Optimizations as Rewrite Strategies
ICFP Program
Bastian Hagedorn University of Münster, Germany, Johannes Lenfers University of Münster, Thomas Koehler University of Glasgow, United Kingdom, Xueying Qin University of Glasgow, United Kingdom, Sergei Gorlatch University of Münster, Germany, Michel Steuwer The University of Edinburgh
DOI Media Attached
02:45
15m
Talk
Staged Selective Parser Combinators
ICFP Program
Jamie Willis Imperial College London, Nicolas Wu Imperial College London, UK, Matthew Pickering University of Bristol, UK
DOI Media Attached
03:00
15m
Talk
Kindly Bent to Free Us
ICFP Program
Gabriel Radanne Inria, Hannes Saffrich University of Freiburg, Peter Thiemann University of Freiburg, Germany
DOI Pre-print Media Attached File Attached
03:15
15m
Talk
Sealing Pointer-Based Optimizations Behind Pure Functions
ICFP Program
Daniel Selsam Microsoft Research, Simon Hudon Carnegie Mellon University, Leonardo de Moura Microsoft Research, n.n.
DOI Media Attached
03:30
15m
Talk
Effects for Efficiency: Asymptotic Speedup with First-Class Control
ICFP Program
Daniel Hillerström The University of Edinburgh, Sam Lindley Heriot-Watt University, UK / The University of Edinburgh, UK, John Longley The University of Edinburgh
DOI Media Attached
03:45
15m
Talk
Computation Focusing
ICFP Program
Nick Rioux University of Pennsylvania, Steve Zdancewic University of Pennsylvania
DOI Media Attached
04:00
15m
Talk
Retrofitting Parallelism onto OCamlDistinguished Paper
ICFP Program
KC Sivaramakrishnan IIT Madras, Stephen Dolan University of Cambridge, UK, Leo White Jane Street, Sadiq Jaffer Opsian and OCaml Labs, Tom Kelly OCaml Labs, Anmol Sahoo IIT Madras, Sudha Parimala IIT Madras, Atul Dhiman IIT Madras, Anil Madhavapeddy OCaml Labs
DOI Media Attached
04:15
15m
Talk
Liquid Information Flow ControlDistinguished Paper
ICFP Program
Nadia Polikarpova University of California, San Diego, Deian Stefan University of California at San Diego, USA, Jean Yang Carnegie Mellon University, Shachar Itzhaky Technion, Israel, Travis Hance Carnegie Mellon University, Armando Solar-Lezama Massachusetts Institute of Technology, USA
DOI Media Attached