SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Fri 20 Nov 2020 12:00 - 12:20 at SPLASH-I - F-3A Chair(s): Stefan Marr, Reuben Rowe
Sat 21 Nov 2020 00:00 - 00:20 at SPLASH-I - F-3A Chair(s): Hidehiko Masuhara, Ramy Shahin

We present a simple, practical, and expressive type and effect system based on Boolean
constraints. The effect system extends the Hindley-Milner type system, supports
parametric polymorphism, and preserves principal types modulo Boolean
equivalence. We show how to support type inference by extending Algorithm W with
Boolean unification based on the successive variable elimination algorithm.

We implement the type and effect system in the Flix programming language. We
perform an in-depth evaluation on the impact of Boolean unification on type
inference time and end-to-end compilation time. While the computational
complexity of Boolean unification is NP-hard, the experimental results
demonstrate that it works well in practice. We find that the impact on type
inference time is on average a 1.4x slowdown and the overall impact on
end-to-end compilation time is a 1.1x slowdown.

Fri 20 Nov

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

11:00 - 12:20
F-3AOOPSLA at SPLASH-I +12h
Chair(s): Stefan Marr University of Kent, Reuben Rowe University College London
11:00
20m
Talk
Contextual Dispatch for Function Specialization
OOPSLA
Olivier Flückiger Northeastern University, Guido Chari Asapp, Ming-Ho Yee Northeastern University, Jan Ječmen Czech Technical University, Jakob Hain Northeastern University, Jan Vitek Northeastern University / Czech Technical University
Link to publication DOI Pre-print Media Attached
11:20
20m
Talk
Fixpoints for the Masses: Programming with First-Class Datalog Constraints
OOPSLA
Magnus Madsen Aarhus University, Ondřej Lhoták University of Waterloo
Link to publication DOI Media Attached
11:40
20m
Talk
Verifying and Improving Halide’s Term Rewriting System with Program Synthesis
OOPSLA
Julie L. Newcomb University of Washington, Andrew Adams Adobe Research, Steven Johnson Google, Rastislav Bodik University of Washington, Shoaib Kamil Adobe Research
Link to publication DOI Media Attached
12:00
20m
Talk
Polymorphic Types and Effects with Boolean Unification
OOPSLA
Magnus Madsen Aarhus University, Jaco van de Pol Aarhus University
Link to publication DOI Media Attached
23:00 - 00:20
F-3AOOPSLA at SPLASH-I
Chair(s): Hidehiko Masuhara Tokyo Institute of Technology, Ramy Shahin University of Toronto
23:00
20m
Talk
Contextual Dispatch for Function Specialization
OOPSLA
Olivier Flückiger Northeastern University, Guido Chari Asapp, Ming-Ho Yee Northeastern University, Jan Ječmen Czech Technical University, Jakob Hain Northeastern University, Jan Vitek Northeastern University / Czech Technical University
Link to publication DOI Pre-print Media Attached
23:20
20m
Talk
Fixpoints for the Masses: Programming with First-Class Datalog Constraints
OOPSLA
Magnus Madsen Aarhus University, Ondřej Lhoták University of Waterloo
Link to publication DOI Media Attached
23:40
20m
Talk
Verifying and Improving Halide’s Term Rewriting System with Program Synthesis
OOPSLA
Julie L. Newcomb University of Washington, Andrew Adams Adobe Research, Steven Johnson Google, Rastislav Bodik University of Washington, Shoaib Kamil Adobe Research
Link to publication DOI Media Attached
00:00
20m
Talk
Polymorphic Types and Effects with Boolean Unification
OOPSLA
Magnus Madsen Aarhus University, Jaco van de Pol Aarhus University
Link to publication DOI Media Attached