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: (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