Write a Blog >>
ICFP 2020
Thu 20 - Fri 28 August 2020
Wed 26 Aug 2020 11:15 - 11:30 at ICFP NY 5 - New York 5 Chair(s): Richard A. Eisenberg
Wed 26 Aug 2020 22:15 - 22:30 at ICFP Asia 5 - Asia 5 Chair(s): Richard A. Eisenberg

This paper presents a simple mechanized formalization of Separation Logic for sequential programs. This formalization is aimed for teaching the ideas of Separation Logic, including its soundness proof and its recent enhancements. The formalization serves as support for a course that follows the style of the successful Software Foundations series, with all the statement and proofs formalized in Coq. This course only assumes basic knowledge of lambda-calculus, semantics and logics, and therefore should be accessible to a broad audience.

Wed 26 Aug
Times are displayed in time zone: Eastern Time (US & Canada) change

11:00 - 13:00: New York 5ICFP Program at ICFP NY 5
Chair(s): Richard A. EisenbergTweag I/O

Public livestreams: YouTube, Bilibili (China)

11:00 - 11:15
Talk
ICFP Program
Joseph W. CutlerWesleyan University, Dan LicataWesleyan University, Norman DannerWesleyan University
DOI
11:15 - 11:30
Talk
ICFP Program
DOI
11:30 - 11:45
Talk
ICFP Program
Aaron StumpThe University of Iowa, USA, Chris JenkinsThe University of Iowa, Stephan SpahnThe University of Iowa, Colin McDonaldUniversity of Notre Dame
DOI
11:45 - 12:00
Talk
ICFP Program
Nandor LickerUniversity of Cambridge, Timothy M. JonesUniversity of Cambridge, UK
DOI Media Attached
12:00 - 12:15
Talk
ICFP Program
Vikraman ChoudhuryIndiana University & University of Cambridge, Neel KrishnaswamiComputer Laboratory, University of Cambridge
DOI
12:15 - 12:30
Talk
ICFP Program
Xiaohong ChenUniversity of Illinois at Urbana-Champaign, Grigore RoşuUniversity of Illinois at Urbana-Champaign
DOI
12:30 - 12:45
Talk
ICFP Program
Pierce DarraghUniversity of Utah, Michael D. AdamsUniversity of Michigan
DOI
12:45 - 13:00
Talk
ICFP Program
Timothée HaudebourgUniv Rennes, Inria, CNRS, IRISA, Thomas GenetIRISA, Univ Rennes, Thomas P. JensenINRIA Rennes
DOI
22:30 - 00:00: Asia 5ICFP Program at ICFP Asia 5
Chair(s): Richard A. EisenbergTweag I/O

Public livestreams: YouTube, Bilibili (China)

22:00 - 22:30
Talk
ICFP Program
Joseph W. CutlerWesleyan University, Dan LicataWesleyan University, Norman DannerWesleyan University
DOI
22:15 - 22:30
Talk
ICFP Program
DOI
22:30 - 22:45
Talk
ICFP Program
Aaron StumpThe University of Iowa, USA, Chris JenkinsThe University of Iowa, Stephan SpahnThe University of Iowa, Colin McDonaldUniversity of Notre Dame
DOI
22:45 - 23:00
Talk
ICFP Program
Nandor LickerUniversity of Cambridge, Timothy M. JonesUniversity of Cambridge, UK
DOI Media Attached
23:00 - 23:15
Talk
ICFP Program
Vikraman ChoudhuryIndiana University & University of Cambridge, Neel KrishnaswamiComputer Laboratory, University of Cambridge
DOI
23:15 - 23:30
Talk
ICFP Program
Xiaohong ChenUniversity of Illinois at Urbana-Champaign, Grigore RoşuUniversity of Illinois at Urbana-Champaign
DOI
23:30 - 23:45
Talk
ICFP Program
Pierce DarraghUniversity of Utah, Michael D. AdamsUniversity of Michigan
DOI
23:45 - 00:00
Talk
ICFP Program
Timothée HaudebourgUniv Rennes, Inria, CNRS, IRISA, Thomas GenetIRISA, Univ Rennes, Thomas P. JensenINRIA Rennes
DOI