Higher-Order Demand-Driven Symbolic Evaluation (ICFP 2020 - Program) - ICFP 2020

Write a Blog >>

Thu 20 - Fri 28 August 2020

Who

Zachary Palmer, Theodore Park, Scott F. Smith, Shiwei Weng

Track

ICFP 2020 ICFP Program

Time Zone

The program is currently displayed in (GMT-04:00) Eastern Time (US & Canada).

Use conference time zone: (GMT-04:00) Eastern Time (US & Canada)Select other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

When

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

Abstract

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.

DOI

https://doi.org/10.1145/3408984

Zachary Palmer

Swarthmore College

United States

Theodore Park

Swarthmore and Hopkins

Scott F. Smith

The Johns Hopkins University

Shiwei Weng

The Johns Hopkins University

YouTube

Time Zone

The program is currently displayed in (GMT-04:00) Eastern Time (US & Canada).

Use conference time zone: (GMT-04:00) Eastern Time (US & Canada)Select other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Session Program

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