SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Fri 20 Nov 2020 10:00 - 10:20 at SPLASH-I - F-2A Chair(s): Aviral Goel, Reuben Rowe
Fri 20 Nov 2020 22:00 - 22:20 at SPLASH-I - F-2A Chair(s): Pranav Kant, Atsushi Igarashi

Automation of fixpoint reasoning has been extensively studied for various mathematical structures, logical formalisms, and computational domains, resulting in specialized fixpoint provers for heaps, for streams, for term algebras, for temporal properties, for program correctness, and for many other formal systems and inductive and coinductive properties. However, in spite of great theoretical and practical interest, there is no unified framework for automated fixpoint reasoning. Although several attempts have been made, there is no evidence that such a unified framework is possible, or practical. In this paper, we propose a candidate based on matching logic, a formalism recently shown to theoretically unify the above mentioned formal systems. Unfortunately, the (Knaster-Tarski) proof rule of matching logic, which enables inductive reasoning, is not syntax-driven. Worse, it can be applied at any step during a proof, making automation seem hopeless. Inspired by recent advances in automation of inductive proofs in separation logic, we propose an alternative proof system for matching logic, which is amenable for automation. We then discuss our implementation of it, which although not superior to specialized state-of-the-art automated provers for specific domains, we believe brings some evidence and hope that a unified framework for automated reasoning is not out of reach.

Fri 20 Nov
Times are displayed in time zone: Central Time (US & Canada) change

09:00 - 10:20: F-2AOOPSLA at SPLASH-I +12h
Chair(s): Aviral GoelNortheastern University, Reuben RoweUniversity College London
09:00 - 09:20
Talk
OOPSLA
Ryan SenanayakeReservoir Labs, Changwan HongMassachusetts Institute of Technology, Ziheng WangMassachusetts Institute of Technology, Amalee WilsonStanford University, Stephen ChouMassachusetts Institute of Technology, Shoaib KamilAdobe Research, Saman AmarasingheMassachusetts Institute of Technology, Fredrik KjolstadStanford University
Link to publication DOI Pre-print Media Attached File Attached
09:20 - 09:40
Talk
OOPSLA
Koar MarntirosianKU Leuven, Tom SchrijversKU Leuven, Bruno C. d. S. OliveiraUniversity of Hong Kong, Georgios KarachaliasTweag
Link to publication DOI Media Attached
09:40 - 10:00
Talk
OOPSLA
Sean BartellUniversity of Illinois at Urbana-Champaign, Will DietzUniversity of Illinois at Urbana-Champaign, Vikram S. AdveUniversity of Illinois at Urbana-Champaign
Link to publication DOI Media Attached
10:00 - 10:20
Talk
OOPSLA
Xiaohong ChenUniversity of Illinois at Urbana-Champaign, Minh-Thai TrinhAdvanced Digital Sciences Center, Nishant RodriguesUniversity of Illinois at Urbana-Champaign, Lucas PeñaUniversity of Illinois at Urbana-Champaign, Grigore RoşuUniversity of Illinois at Urbana-Champaign
Link to publication DOI Media Attached
21:00 - 22:20: F-2AOOPSLA at SPLASH-I
Chair(s): Pranav KantUniversity of Utah, Atsushi IgarashiKyoto University, Japan
21:00 - 21:20
Talk
OOPSLA
Ryan SenanayakeReservoir Labs, Changwan HongMassachusetts Institute of Technology, Ziheng WangMassachusetts Institute of Technology, Amalee WilsonStanford University, Stephen ChouMassachusetts Institute of Technology, Shoaib KamilAdobe Research, Saman AmarasingheMassachusetts Institute of Technology, Fredrik KjolstadStanford University
Link to publication DOI Pre-print Media Attached File Attached
21:20 - 21:40
Talk
OOPSLA
Koar MarntirosianKU Leuven, Tom SchrijversKU Leuven, Bruno C. d. S. OliveiraUniversity of Hong Kong, Georgios KarachaliasTweag
Link to publication DOI Media Attached
21:40 - 22:00
Talk
OOPSLA
Sean BartellUniversity of Illinois at Urbana-Champaign, Will DietzUniversity of Illinois at Urbana-Champaign, Vikram S. AdveUniversity of Illinois at Urbana-Champaign
Link to publication DOI Media Attached
22:00 - 22:20
Talk
OOPSLA
Xiaohong ChenUniversity of Illinois at Urbana-Champaign, Minh-Thai TrinhAdvanced Digital Sciences Center, Nishant RodriguesUniversity of Illinois at Urbana-Champaign, Lucas PeñaUniversity of Illinois at Urbana-Champaign, Grigore RoşuUniversity of Illinois at Urbana-Champaign
Link to publication DOI Media Attached