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

Symbolic backwards execution (SBE) is a useful variation on standard forward symbolic evaluation; it allows a symbolic evaluation to start anywhere in the program and proceed by executing in reverse to the program start. SBE brings goal-directed reasoning to symbolic evaluation and has proven effective in e.g. automated test generation for imperative languages.

In this paper we define DDSE, a novel SBE which operates on a functional as opposed to imperative language; furthermore, it is defined as a natural extension of a backwards-executing interpreter. We establish the soundness of DDSE and define a test generation algorithm for this toy language. We report on an initial reference implementation to confirm the correctness of the principles.

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 Chlipala Massachusetts Institute of Technology

Public livestreams: YouTube, Bilibili (China)

11:30
15m
Talk
Stable Relations and Abstract Interpretation of Higher-Order Programs
ICFP Program
Benoît Montagu Inria, Thomas P. Jensen INRIA Rennes
DOI Media Attached File Attached
11:45
15m
Talk
Higher-Order Demand-Driven Symbolic Evaluation
ICFP Program
Zachary Palmer Swarthmore College, Theodore Park Swarthmore and Hopkins, Scott F. Smith The Johns Hopkins University, Shiwei Weng The Johns Hopkins University
DOI Media Attached
12:00
15m
Talk
Sparcl: A Language for Partially-Invertible Computation
ICFP Program
Kazutaka Matsuda Tohoku University, Japan, Meng Wang University of Bristol, UK
DOI Media Attached
12:15
15m
Talk
SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs
ICFP Program
Nikhil Swamy Microsoft Research, Aseem Rastogi Microsoft Research, Aymeric Fromherz Carnegie Mellon University, Denis Merigoux INRIA, Danel Ahman University of Ljubljana, Guido Martínez CIFASIS-CONICET, Argentina
DOI Media Attached
12:30
15m
Talk
TLC: Temporal Logic of Distributed Components
ICFP Program
Jeremiah Griffin University of California, Riverside, Mohsen Lesani University of California, Riverside, Narges Shadab University of California, Riverside, Xizhe Yin Univsersity of California, Riverside
DOI Media Attached
12:45
15m
Talk
Effect Handlers, Evidently
ICFP Program
Ningning Xie University of Toronto, Jonathan Immanuel Brachthäuser University of Tübingen, Germany, Daniel Hillerström The University of Edinburgh, Philipp Schuster University of Tübingen, Germany, Daan Leijen Microsoft Research, USA
DOI Media Attached
22:30 - 00:00
Asia 1ICFP Program at ICFP Asia 1
Chair(s): Adam Chlipala Massachusetts Institute of Technology

Public livestreams: YouTube, Bilibili (China)

22:30
15m
Talk
Stable Relations and Abstract Interpretation of Higher-Order Programs
ICFP Program
Benoît Montagu Inria, Thomas P. Jensen INRIA Rennes
DOI Media Attached File Attached
22:45
15m
Talk
Higher-Order Demand-Driven Symbolic Evaluation
ICFP Program
Zachary Palmer Swarthmore College, Theodore Park Swarthmore and Hopkins, Scott F. Smith The Johns Hopkins University, Shiwei Weng The Johns Hopkins University
DOI Media Attached
23:00
15m
Talk
Sparcl: A Language for Partially-Invertible Computation
ICFP Program
Kazutaka Matsuda Tohoku University, Japan, Meng Wang University of Bristol, UK
DOI Media Attached
23:15
15m
Talk
SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs
ICFP Program
Nikhil Swamy Microsoft Research, Aseem Rastogi Microsoft Research, Aymeric Fromherz Carnegie Mellon University, Denis Merigoux INRIA, Danel Ahman University of Ljubljana, Guido Martínez CIFASIS-CONICET, Argentina
DOI Media Attached
23:30
15m
Talk
TLC: Temporal Logic of Distributed Components
ICFP Program
Jeremiah Griffin University of California, Riverside, Mohsen Lesani University of California, Riverside, Narges Shadab University of California, Riverside, Xizhe Yin Univsersity of California, Riverside
DOI Media Attached
23:45
15m
Talk
Effect Handlers, Evidently
ICFP Program
Ningning Xie University of Toronto, Jonathan Immanuel Brachthäuser University of Tübingen, Germany, Daniel Hillerström The University of Edinburgh, Philipp Schuster University of Tübingen, Germany, Daan Leijen Microsoft Research, USA
DOI Media Attached