Write a Blog >>
ICFP 2020
Thu 20 - Fri 28 August 2020
Mon 24 Aug 2020 12:45 - 13:00 at ICFP NY 1 - New York 1 Chair(s): Adam Chlipala
Mon 24 Aug 2020 23:45 - 00:00 at ICFP Asia 1 - Asia 1 Chair(s): Adam Chlipala

Algebraic effect handlers are a powerful way to incorporate effects in a programming language. Sometimes perhaps even too powerful. In this article we define a restriction of general effect handlers with scoped resumptions. We argue one can still express all important effects, while improving local reasoning about effect handlers. Using the newly gained guarantees, we define a sound and coherent evidence translation for effect handlers which directly passes the handlers as evidence to each operation. We prove full soundness and coherence of the translation into plain lambda calculus. The evidence in turn enables efficient implementations of effect operations; in particular, we show we can execute tail-resumptive operations in place (without needing to capture the evaluation context), and how we can replace the runtime search for a handler by indexing with a constant offset.

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

icfp-2020-papers
11:30 - 13:00: ICFP Program - New York 1 at ICFP NY 1
Chair(s): Adam ChlipalaMassachusetts Institute of Technology

Public livestreams: YouTube, Bilibili (China)

icfp-2020-papers11:30 - 11:45
Talk
DOI Media Attached File Attached
icfp-2020-papers11:45 - 12:00
Talk
Zachary PalmerSwarthmore College, Theodore ParkSwarthmore and Hopkins, Scott F. SmithThe Johns Hopkins University, Shiwei WengThe Johns Hopkins University
DOI
icfp-2020-papers12:00 - 12:15
Talk
Kazutaka MatsudaTohoku University, Japan, Meng WangUniversity of Bristol, UK
DOI
icfp-2020-papers12:15 - 12:30
Talk
Nikhil SwamyMicrosoft Research, Aseem RastogiMicrosoft Research, Aymeric FromherzCarnegie Mellon University, Denis MerigouxINRIA, Danel AhmanUniversity of Ljubljana, Guido MartínezCIFASIS-CONICET, Argentina
DOI
icfp-2020-papers12:30 - 12:45
Talk
Jeremiah GriffinUniversity of California, Riverside, Mohsen LesaniUniversity of California, Riverside, Narges ShadabUniversity of California, Riverside, Xizhe YinUnivsersity of California, Riverside
DOI
icfp-2020-papers12:45 - 13:00
Talk
Ningning XieMicrosoft Research, USA, Jonathan Immanuel BrachthäuserUniversity of Tübingen, Germany, Daniel HillerströmThe University of Edinburgh, Philipp SchusterUniversity of Tübingen, Germany, Daan LeijenMicrosoft Research, USA
DOI
icfp-2020-papers
22:30 - 00:00: ICFP Program - Asia 1 at ICFP Asia 1
Chair(s): Adam ChlipalaMassachusetts Institute of Technology

Public livestreams: YouTube, Bilibili (China)

icfp-2020-papers22:30 - 22:45
Talk
DOI Media Attached File Attached
icfp-2020-papers22:45 - 23:00
Talk
Zachary PalmerSwarthmore College, Theodore ParkSwarthmore and Hopkins, Scott F. SmithThe Johns Hopkins University, Shiwei WengThe Johns Hopkins University
DOI
icfp-2020-papers23:00 - 23:15
Talk
Kazutaka MatsudaTohoku University, Japan, Meng WangUniversity of Bristol, UK
DOI
icfp-2020-papers23:15 - 23:30
Talk
Nikhil SwamyMicrosoft Research, Aseem RastogiMicrosoft Research, Aymeric FromherzCarnegie Mellon University, Denis MerigouxINRIA, Danel AhmanUniversity of Ljubljana, Guido MartínezCIFASIS-CONICET, Argentina
DOI
icfp-2020-papers23:30 - 23:45
Talk
Jeremiah GriffinUniversity of California, Riverside, Mohsen LesaniUniversity of California, Riverside, Narges ShadabUniversity of California, Riverside, Xizhe YinUnivsersity of California, Riverside
DOI
icfp-2020-papers23:45 - 00:00
Talk
Ningning XieMicrosoft Research, USA, Jonathan Immanuel BrachthäuserUniversity of Tübingen, Germany, Daniel HillerströmThe University of Edinburgh, Philipp SchusterUniversity of Tübingen, Germany, Daan LeijenMicrosoft Research, USA
DOI