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

Resolution and subtyping are two common mechanisms in programming languages. Resolution is used by features such as type classes or Scala-style implicits to synthesize values automatically from contextual type information. Subtyping is commonly used to automatically convert the type of a value into another compatible type. So far the two mechanisms have been considered independently of each other. This paper shows that, with a small extension, subtyping with intersection types can subsume resolution. This has three main consequences. Firstly, resolution does not need to be implemented as a separate mechanism. Secondly, the interaction between resolution and subtyping becomes apparent. Finally, the integration of resolution into subtyping enables first-class (implicit) environments. The extension that recovers the power of resolution via subtyping is the modus ponens rule of propositional logic. While it is easily added to declarative subtyping, significant care needs to be taken to retain desirable properties, such as transitivity and decidability of algorithmic subtyping, and coherence. To materialize these ideas we develop $\lambda_i^{MP}$, a calculus that extends a iprevious calculus with disjoint intersection types, and develop its metatheory in the Coq theorem prover.

Fri 20 Nov

Displayed time zone: Central Time (US & Canada) change

09:00 - 10:20
F-2AOOPSLA at SPLASH-I +12h
Chair(s): Aviral Goel Northeastern University, Reuben Rowe University College London
09:00
20m
Talk
A Sparse Iteration Space Transformation Framework for Sparse Tensor Algebra
OOPSLA
Ryan Senanayake Reservoir Labs, Changwan Hong Massachusetts Institute of Technology, Ziheng Wang Massachusetts Institute of Technology, Amalee Wilson Stanford University, Stephen Chou Massachusetts Institute of Technology, Shoaib Kamil Adobe Research, Saman Amarasinghe Massachusetts Institute of Technology, Fredrik Kjolstad Stanford University
Link to publication DOI Pre-print Media Attached File Attached
09:20
20m
Talk
Resolution as Intersection Subtyping via Modus Ponens
OOPSLA
Koar Marntirosian KU Leuven, Tom Schrijvers KU Leuven, Bruno C. d. S. Oliveira University of Hong Kong, Georgios Karachalias Tweag
Link to publication DOI Media Attached
09:40
20m
Talk
Guided Linking: Dynamic Linking without the Costs
OOPSLA
Sean Bartell University of Illinois at Urbana-Champaign, Will Dietz University of Illinois at Urbana-Champaign, Vikram S. Adve University of Illinois at Urbana-Champaign
Link to publication DOI Media Attached
10:00
20m
Talk
Towards a Unified Proof Framework for Automated Fixpoint Reasoning using Matching Logic
OOPSLA
Xiaohong Chen University of Illinois at Urbana-Champaign, Minh-Thai Trinh Advanced Digital Sciences Center, Nishant Rodrigues University of Illinois at Urbana-Champaign, Lucas Peña University of Illinois at Urbana-Champaign, Grigore Roşu University of Illinois at Urbana-Champaign
Link to publication DOI Media Attached
21:00 - 22:20
F-2AOOPSLA at SPLASH-I
Chair(s): Pranav Kant University of Utah, Atsushi Igarashi Kyoto University, Japan
21:00
20m
Talk
A Sparse Iteration Space Transformation Framework for Sparse Tensor Algebra
OOPSLA
Ryan Senanayake Reservoir Labs, Changwan Hong Massachusetts Institute of Technology, Ziheng Wang Massachusetts Institute of Technology, Amalee Wilson Stanford University, Stephen Chou Massachusetts Institute of Technology, Shoaib Kamil Adobe Research, Saman Amarasinghe Massachusetts Institute of Technology, Fredrik Kjolstad Stanford University
Link to publication DOI Pre-print Media Attached File Attached
21:20
20m
Talk
Resolution as Intersection Subtyping via Modus Ponens
OOPSLA
Koar Marntirosian KU Leuven, Tom Schrijvers KU Leuven, Bruno C. d. S. Oliveira University of Hong Kong, Georgios Karachalias Tweag
Link to publication DOI Media Attached
21:40
20m
Talk
Guided Linking: Dynamic Linking without the Costs
OOPSLA
Sean Bartell University of Illinois at Urbana-Champaign, Will Dietz University of Illinois at Urbana-Champaign, Vikram S. Adve University of Illinois at Urbana-Champaign
Link to publication DOI Media Attached
22:00
20m
Talk
Towards a Unified Proof Framework for Automated Fixpoint Reasoning using Matching Logic
OOPSLA
Xiaohong Chen University of Illinois at Urbana-Champaign, Minh-Thai Trinh Advanced Digital Sciences Center, Nishant Rodrigues University of Illinois at Urbana-Champaign, Lucas Peña University of Illinois at Urbana-Champaign, Grigore Roşu University of Illinois at Urbana-Champaign
Link to publication DOI Media Attached