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

We present a novel denotational semantics for the untyped call-by-value $\lambda$-calculus, where terms are interpreted as \emph{stable relations}, \ie as binary relations between substitutions and values, enjoying a monotonicity property. The denotation captures the input-output behaviour of higher-order programs, and is proved sound and complete with respect to the operational semantics. The definition also admits a presentation as a program logic. Following the principles of abstract interpretation, we use our denotational semantics as a \emph{collecting semantics} to derive a modular \emph{relational} analysis for higher-order programs. The analysis infers equalities between the arguments of a program and its result—a form of \emph{frame condition} for functional programs.

Slides (icfp2020_slides.pdf)693KiB

Mon 24 Aug
Times are displayed in 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 - 11:45
Talk
Stable Relations and Abstract Interpretation of Higher-Order Programs
ICFP Program
DOI Media Attached File Attached
11:45 - 12:00
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 - 12:15
Talk
Sparcl: A Language for Partially-Invertible Computation
ICFP Program
Kazutaka MatsudaTohoku University, Japan, Meng WangUniversity of Bristol, UK
DOI Media Attached
12:15 - 12:30
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 - 12:45
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 - 13:00
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 - 22:45
Talk
Stable Relations and Abstract Interpretation of Higher-Order Programs
ICFP Program
DOI Media Attached File Attached
22:45 - 23:00
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 - 23:15
Talk
Sparcl: A Language for Partially-Invertible Computation
ICFP Program
Kazutaka MatsudaTohoku University, Japan, Meng WangUniversity of Bristol, UK
DOI Media Attached
23:15 - 23:30
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 - 23:45
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 - 00:00
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