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

Focusing is a technique from proof theory that exploits type information to prune inessential nondeterminism from proof search procedures. Viewed through the lens of the Curry-Howard correspondence, a focused typing derivation yields terms in normal form. This paper explores how to exploit focusing for reasoning about contextual equivalences and full abstraction. We present a focused polymorphic call-by-push-value calculus and prove a computational completeness result: for every well-typed term, there exists a focused term that is βη-equivalent to it. This completeness result yields a powerful way to refine the context lemmas for establishing contextual equivalences, cutting down the set that must be considered to just focused contexts. The paper demonstrates the application of focusing to establish program equivalences, including free theorems. It also uses focusing to prove full abstraction of a translation of the pure, total call-by-push-value language into a language with divergence and simple effect types, yielding a novel solution to a simple-to-state, but hitherto difficult to solve problem.

Mon 24 Aug
Times are displayed in time zone: Eastern Time (US & Canada) change

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

Public livestreams: YouTube, Bilibili (China)

14:30 - 14:45
Talk
Achieving High-Performance the Functional Way - A Functional Pearl on Expressing High-Performance Optimizations as Rewrite Strategies
ICFP Program
Bastian HagedornUniversity of Münster, Germany, Johannes LenfersUniversity of Münster, Thomas KoehlerUniversity of Glasgow, United Kingdom, Xueying QinUniversity of Glasgow, United Kingdom, Sergei GorlatchUniversity of Münster, Germany, Michel SteuwerThe University of Edinburgh
DOI Media Attached
14:45 - 15:00
Talk
Staged Selective Parser Combinators
ICFP Program
Jamie WillisImperial College London, Nicolas WuImperial College London, UK, Matthew PickeringUniversity of Bristol, UK
DOI Media Attached
15:00 - 15:15
Talk
Kindly Bent to Free Us
ICFP Program
Gabriel RadanneInria, Hannes SaffrichUniversity of Freiburg, Peter ThiemannUniversity of Freiburg, Germany
DOI Pre-print Media Attached File Attached
15:15 - 15:30
Talk
Sealing Pointer-Based Optimizations Behind Pure Functions
ICFP Program
Daniel SelsamMicrosoft Research, Simon HudonCarnegie Mellon University, Leonardo De MouraMicrosoft Research, n.n.
DOI Media Attached
15:30 - 15:45
Talk
Effects for Efficiency: Asymptotic Speedup with First-Class Control
ICFP Program
Daniel HillerströmThe University of Edinburgh, Sam LindleyHeriot-Watt University, UK / The University of Edinburgh, UK, John LongleyThe University of Edinburgh
DOI Media Attached
15:45 - 16:00
Talk
Computation Focusing
ICFP Program
Nick RiouxUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania
DOI Media Attached
16:00 - 16:15
Talk
Retrofitting Parallelism onto OCamlDistinguished Paper
ICFP Program
KC SivaramakrishnanIIT Madras, Stephen DolanUniversity of Cambridge, UK, Leo WhiteJane Street, Sadiq JafferOpsian and OCaml Labs, Tom KellyOCaml Labs, Anmol SahooIIT Madras, Sudha ParimalaIIT Madras, Atul DhimanIIT Madras, Anil MadhavapeddyOCaml Labs
DOI Media Attached
16:15 - 16:30
Talk
Liquid Information Flow ControlDistinguished Paper
ICFP Program
Nadia PolikarpovaUniversity of California, San Diego, Deian StefanUniversity of California at San Diego, USA, Jean YangCarnegie Mellon University, Shachar ItzhakyTechnion, Israel, Travis HanceCarnegie Mellon University, Armando Solar-LezamaMassachusetts Institute of Technology, USA
DOI Media Attached

Tue 25 Aug
Times are displayed in time zone: Eastern Time (US & Canada) change

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

Public livestreams: YouTube, Bilibili (China)

02:30 - 02:45
Talk
Achieving High-Performance the Functional Way - A Functional Pearl on Expressing High-Performance Optimizations as Rewrite Strategies
ICFP Program
Bastian HagedornUniversity of Münster, Germany, Johannes LenfersUniversity of Münster, Thomas KoehlerUniversity of Glasgow, United Kingdom, Xueying QinUniversity of Glasgow, United Kingdom, Sergei GorlatchUniversity of Münster, Germany, Michel SteuwerThe University of Edinburgh
DOI Media Attached
02:45 - 03:00
Talk
Staged Selective Parser Combinators
ICFP Program
Jamie WillisImperial College London, Nicolas WuImperial College London, UK, Matthew PickeringUniversity of Bristol, UK
DOI Media Attached
03:00 - 03:15
Talk
Kindly Bent to Free Us
ICFP Program
Gabriel RadanneInria, Hannes SaffrichUniversity of Freiburg, Peter ThiemannUniversity of Freiburg, Germany
DOI Pre-print Media Attached File Attached
03:15 - 03:30
Talk
Sealing Pointer-Based Optimizations Behind Pure Functions
ICFP Program
Daniel SelsamMicrosoft Research, Simon HudonCarnegie Mellon University, Leonardo De MouraMicrosoft Research, n.n.
DOI Media Attached
03:30 - 03:45
Talk
Effects for Efficiency: Asymptotic Speedup with First-Class Control
ICFP Program
Daniel HillerströmThe University of Edinburgh, Sam LindleyHeriot-Watt University, UK / The University of Edinburgh, UK, John LongleyThe University of Edinburgh
DOI Media Attached
03:45 - 04:00
Talk
Computation Focusing
ICFP Program
Nick RiouxUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania
DOI Media Attached
04:00 - 04:15
Talk
Retrofitting Parallelism onto OCamlDistinguished Paper
ICFP Program
KC SivaramakrishnanIIT Madras, Stephen DolanUniversity of Cambridge, UK, Leo WhiteJane Street, Sadiq JafferOpsian and OCaml Labs, Tom KellyOCaml Labs, Anmol SahooIIT Madras, Sudha ParimalaIIT Madras, Atul DhimanIIT Madras, Anil MadhavapeddyOCaml Labs
DOI Media Attached
04:15 - 04:30
Talk
Liquid Information Flow ControlDistinguished Paper
ICFP Program
Nadia PolikarpovaUniversity of California, San Diego, Deian StefanUniversity of California at San Diego, USA, Jean YangCarnegie Mellon University, Shachar ItzhakyTechnion, Israel, Travis HanceCarnegie Mellon University, Armando Solar-LezamaMassachusetts Institute of Technology, USA
DOI Media Attached