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

Invertibility is a fundamental concept in computer science, with various manifestations in software development (serializer/deserializer, parser/printer, redo/undo, compressor/decompressor, and so on). Full invertibility necessarily requires bijectivity, but the direct approach of composing bijective functions to develop invertible programs is too restrictive to be useful. In this paper, we take a different approach by focusing on \emph{partially-invertible} functions—functions that become invertible if some of their arguments are fixed. The simplest example of such is addition, which becomes invertible when fixing one of the operands. More involved examples include entropy-based compression methods (e.g., Huffman coding), which carry the occurrence frequency of input symbols (in certain formats such as Huffman tree), and fixing this frequency information makes the compression methods invertible.

We develop a language Sparcl for programming such functions in a natural way, where partial-invertibility is the norm and bijectivity is a special case, hence gaining significant expressiveness without compromising correctness. The challenge in designing such a language is to allow ordinary programming (the "partially'' part) to interact with the invertible part freely, and yet guarantee invertibility by construction. The language Sparcl is linear-typed, and has a type constructor to distinguish data that are subject to invertible computation and those that are not. We present the syntax, type system, and semantics of the language, and prove that Sparcl correctly guarantees invertibility for its programs. We demonstrate the usefulness of Sparcl with examples including tree rebuilding from preorder and inorder traversals and Huffman coding.

Conference Day
Mon 24 Aug

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

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

Public livestreams: YouTube, Bilibili (China)

11:30
15m
Talk
Stable Relations and Abstract Interpretation of Higher-Order Programs
ICFP Program
DOI Media Attached File Attached
11:45
15m
Talk
Higher-Order Demand-Driven Symbolic Evaluation
ICFP Program
Zachary PalmerSwarthmore College, Theodore ParkSwarthmore and Hopkins, Scott F. SmithThe Johns Hopkins University, Shiwei WengThe Johns Hopkins University
DOI Media Attached
12:00
15m
Talk
Sparcl: A Language for Partially-Invertible Computation
ICFP Program
Kazutaka MatsudaTohoku University, Japan, Meng WangUniversity of Bristol, UK
DOI Media Attached
12:15
15m
Talk
SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs
ICFP Program
Nikhil SwamyMicrosoft Research, Aseem RastogiMicrosoft Research, Aymeric FromherzCarnegie Mellon University, Denis MerigouxINRIA, Danel AhmanUniversity of Ljubljana, Guido MartínezCIFASIS-CONICET, Argentina
DOI Media Attached
12:30
15m
Talk
TLC: Temporal Logic of Distributed Components
ICFP Program
Jeremiah GriffinUniversity of California, Riverside, Mohsen LesaniUniversity of California, Riverside, Narges ShadabUniversity of California, Riverside, Xizhe YinUnivsersity of California, Riverside
DOI Media Attached
12:45
15m
Talk
Effect Handlers, Evidently
ICFP Program
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 Media Attached
22:30 - 00:00
Asia 1ICFP Program at ICFP Asia 1
Chair(s): Adam ChlipalaMassachusetts Institute of Technology

Public livestreams: YouTube, Bilibili (China)

22:30
15m
Talk
Stable Relations and Abstract Interpretation of Higher-Order Programs
ICFP Program
DOI Media Attached File Attached
22:45
15m
Talk
Higher-Order Demand-Driven Symbolic Evaluation
ICFP Program
Zachary PalmerSwarthmore College, Theodore ParkSwarthmore and Hopkins, Scott F. SmithThe Johns Hopkins University, Shiwei WengThe Johns Hopkins University
DOI Media Attached
23:00
15m
Talk
Sparcl: A Language for Partially-Invertible Computation
ICFP Program
Kazutaka MatsudaTohoku University, Japan, Meng WangUniversity of Bristol, UK
DOI Media Attached
23:15
15m
Talk
SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs
ICFP Program
Nikhil SwamyMicrosoft Research, Aseem RastogiMicrosoft Research, Aymeric FromherzCarnegie Mellon University, Denis MerigouxINRIA, Danel AhmanUniversity of Ljubljana, Guido MartínezCIFASIS-CONICET, Argentina
DOI Media Attached
23:30
15m
Talk
TLC: Temporal Logic of Distributed Components
ICFP Program
Jeremiah GriffinUniversity of California, Riverside, Mohsen LesaniUniversity of California, Riverside, Narges ShadabUniversity of California, Riverside, Xizhe YinUnivsersity of California, Riverside
DOI Media Attached
23:45
15m
Talk
Effect Handlers, Evidently
ICFP Program
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 Media Attached