SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Wed 30 Nov 2022 04:45 - 05:00 at Virtual Airmeet Room - Session 1 Chair(s): Amal Ahmed, Jan Vitek

Dependency analysis is vital to several applications in computer science. It lies at the essence of secure information flow analysis, binding-time analysis, etc. Various calculi have been proposed in the literature for analysing individual dependencies. Abadi et. al., by extending Moggi's monadic metalanguage, unified several of these calculi into the Dependency Core Calculus (DCC). DCC has served as a foundational framework for dependency analysis for the last two decades. However, in spite of its success, DCC has its limitations. First, the monadic bind rule of the calculus is nonstandard and relies upon an auxiliary protection judgement. Second, being of a monadic nature, the calculus cannot capture dependency analyses that possess a comonadic nature, for example, the binding-time calculus, $\lambda^{\circ}$, of Davies. In this paper, we address these limitations by designing an alternative dependency calculus that is inspired by standard ideas from category theory. Our calculus is both monadic and comonadic in nature and subsumes both DCC and $\lambda^{\circ}$. Our construction explains the nonstandard bind rule and the protection judgement of DCC in terms of standard categorical concepts. It also leads to a novel technique for proving correctness of dependency analysis. We use this technique to present alternative proofs of correctness for DCC and $\lambda^{\circ}$.

Wed 30 Nov

Displayed time zone: Auckland, Wellington change

04:00 - 05:30
Session 1V-OOPSLA at Virtual Airmeet Room
Chair(s): Amal Ahmed Northeastern University, USA, Jan Vitek Northeastern University
04:00
15m
Talk
Generic Go to Go: Dictionary-Passing, Monomorphisation, and HybridPre-recorded
V-OOPSLA
Stephen Ellis Imperial College London, Shuofei Zhu Pennsylvania State University, Nobuko Yoshida University of Oxford, Linhai Song Pennsylvania State University
DOI
04:15
15m
Research paper
Coverage-guided tensor compiler fuzzing with joint IR-pass mutationPre-recorded
V-OOPSLA
Jiawei Liu University of Illinois at Urbana-Champaign, Yuxiang Wei Tongji University, Sen Yang Fudan University, Yinlin Deng University of Illinois at Urbana-Champaign, Lingming Zhang University of Illinois at Urbana-Champaign
DOI
04:30
15m
Talk
Modular Verification of Op-Based CRDTs in Separation Logic
V-OOPSLA
Abel Nieto Aarhus University, Léon Gondelman Aarhus University, Alban Reynaud ENS Lyon, Amin Timany Aarhus University, Lars Birkedal Aarhus University
DOI
04:45
15m
Talk
Monadic and Comonadic Aspects of Dependency Analysis
V-OOPSLA
Pritam Choudhury University of Pennsylvania
DOI
05:00
30m
Live Q&A
Q&A for Session 1
V-OOPSLA