Write a Blog >>
ICFP 2020
Thu 20 - Fri 28 August 2020
Tue 25 Aug 2020 12:15 - 12:26 at ICFP NY 3 - New York 3 (JFP talks) Chair(s): Jeremy Gibbons
Tue 25 Aug 2020 23:15 - 23:26 at ICFP Asia 3 - Asia 3 (JFP talks) Chair(s): Jeremy Gibbons

We propose a new collection of benchmark problems in mechanizing the metatheory of programming languages, in order to compare and push the state of the art of proof assistants. In particular, we focus on proofs using logical relations (LRs) and propose establishing strong normalization of a simply typed calculus with a proof by Kripke-style LRs as a benchmark. We give a modern view of this well-understood problem by formulating our LR on well-typed terms. Using this case study, we share some of the lessons learned tackling this problem in different dependently typed proof environments. In particular, we consider the mechanization in Beluga, a proof environment that supports higher-order abstract syntax encodings and contrast it to the development and strategies used in general-purpose proof assistants such as Coq and Agda. The goal of this paper is to engage the community in discussions on what support in proof environments is needed to truly bring mechanized metatheory to the masses and engage said community in the crafting of future benchmarks.

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

11:30 - 13:00: New York 3 (JFP talks)ICFP Program at ICFP NY 3
Chair(s): Jeremy GibbonsDepartment of Computer Science, University of Oxford

Public livestreams: YouTube, Bilibili (China)

11:30 - 11:41
Talk
ICFP Program
DOI
11:41 - 11:52
Talk
ICFP Program
Álvaro García PerezIMDEA Software Institute, Pablo NogueiraESNE University School of Design, Innovation and Technology
DOI
11:52 - 12:03
Talk
ICFP Program
Žiga Lukšič, Matija PretnarUniversity of Ljubljana, Slovenia
DOI
12:03 - 12:15
Talk
ICFP Program
Wouter SwierstraUtrecht University, Netherlands
DOI
12:15 - 12:26
Talk
ICFP Program
Andreas AbelGothenburg University, Guillaume AllaisUniversity of St Andrews, Aliya HameerMcGill University, Brigitte PientkaMcGill University, Alberto Momigliano Università degli Studi di Milano, Steven SchäferGoogle, Aarhus, Kathrin StarkPrinceton University, USA
DOI
12:26 - 12:37
Talk
ICFP Program
Oleksandr Manzyuk, Barak A. PearlmutterMaynooth University, Alexey Radul, David Rush, Jeffrey Mark SiskindSchool of Electrical and Computer Engineering, Purdue University
DOI
12:37 - 12:48
Talk
ICFP Program
Matt McCutchen, Judith Borghouts, Andrew D. GordonMicrosoft Research and University of Edinburgh, Simon Peyton JonesMicrosoft, UK, Advait SarkarMicrosoft Research and University of Cambridge
DOI Pre-print Media Attached
12:48 - 13:00
Talk
ICFP Program
DOI
22:30 - 00:00: Asia 3 (JFP talks)ICFP Program at ICFP Asia 3
Chair(s): Jeremy GibbonsDepartment of Computer Science, University of Oxford

Public livestreams: YouTube, Bilibili (China)

22:30 - 22:41
Talk
ICFP Program
DOI
22:41 - 22:52
Talk
ICFP Program
Álvaro García PerezIMDEA Software Institute, Pablo NogueiraESNE University School of Design, Innovation and Technology
DOI
22:52 - 23:03
Talk
ICFP Program
Žiga Lukšič, Matija PretnarUniversity of Ljubljana, Slovenia
DOI
23:03 - 23:15
Talk
ICFP Program
Wouter SwierstraUtrecht University, Netherlands
DOI
23:15 - 23:26
Talk
ICFP Program
Andreas AbelGothenburg University, Guillaume AllaisUniversity of St Andrews, Aliya HameerMcGill University, Brigitte PientkaMcGill University, Alberto Momigliano Università degli Studi di Milano, Steven SchäferGoogle, Aarhus, Kathrin StarkPrinceton University, USA
DOI
23:26 - 23:37
Talk
ICFP Program
Oleksandr Manzyuk, Barak A. PearlmutterMaynooth University, Alexey Radul, David Rush, Jeffrey Mark SiskindSchool of Electrical and Computer Engineering, Purdue University
DOI
23:37 - 23:48
Talk
ICFP Program
Matt McCutchen, Judith Borghouts, Andrew D. GordonMicrosoft Research and University of Edinburgh, Simon Peyton JonesMicrosoft, UK, Advait SarkarMicrosoft Research and University of Cambridge
DOI Pre-print Media Attached
23:48 - 00:00
Talk
ICFP Program
DOI