SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Sun 15 Nov 2020 08:20 - 09:00 at SPLASH-VII - Posters Session 1
Sun 15 Nov 2020 20:20 - 21:00 at SPLASH-VII - Posters Session 1 Mirror

In domains that deal with physical space and geometry, programmers need to track the coordinate systems that underpin a computation. We identify a class of geometry bugs that arise from confusing which coordinate system a vector belongs to. These bugs are not ruled out by current languages for vector-oriented computing, are difficult to check for at run time, and can generate subtly incorrect output that can be hard to test for.

We introduce a type system and language that prevents geometry bugs by reflecting the coordinate system for each geometric object. A value’s geometry type encodes its reference frame, the kind of geometric object (such as a point or a direction), and the computational representation (such as Cartesian or spherical coordinates). We show how these types can rule out geometrically incorrect operations, and we show how to use them to automatically generate correct-by-construction code to transform vectors between coordinate systems. We implement a language for graphics programming, Gator, that checks geometry types and compiles to OpenGL’s shading language, GLSL. Using case studies, we demonstrate that Gator can raise the level of abstraction for shader programming and prevent common errors without inducing significant annotation overhead or performance cost.

Sun 15 Nov

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

08:20 - 09:00
Posters Session 1Posters at SPLASH-VII +12h
08:20
40m
Poster
Formulog: Datalog for SMT-based Static AnalysisOOPSLA
Posters
Aaron Bembenek Harvard University, Michael Greenberg Pomona College, Stephen Chong Harvard University
08:20
40m
Poster
Analogy-Making as a Core Primitive in the Software Engineering ToolboxOnward! Papers
Posters
Matthew Sotoudeh University of California, Davis, Aditya V. Thakur University of California, Davis
08:20
40m
Poster
Row and Bounded Polymorphism via Disjoint PolymorphismECOOP
Posters
Ningning Xie The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong, Xuan Bi The University of Hong Kong, Tom Schrijvers KU Leuven
08:20
40m
Poster
Gradual Verification of Recursive Heap Data StructuresOOPSLA
Posters
Jenna Wise (DiVincenzo) Carnegie Mellon University, Johannes Bader Jane Street, Cameron Wong Jane Street, Jonathan Aldrich Carnegie Mellon University, Éric Tanter University of Chile, Joshua Sunshine Carnegie Mellon University
08:20
40m
Poster
Knowing When to Ask: Sound Scheduling of Name Resolution in Type Checkers Derived from Declarative SpecificationsOOPSLA
Posters
Arjen Rouvoet Delft University of Technology, Hendrik van Antwerpen Delft University of Technology, Casper Bach Poulsen Delft University of Technology, Robbert Krebbers Radboud University Nijmegen, Eelco Visser Delft University of Technology
08:20
40m
Poster
Owicki-Gries Reasoning for C11 RARECOOP
Posters
Sadegh Dalvandi University of Surrey, Simon Doherty University of Sheffield, Brijesh Dongol University of Surrey, Heike Wehrheim Paderborn University
08:20
40m
Poster
Demystifying DependenceOnward! Papers
Posters
08:20
40m
Poster
Can Advanced Type Systems Be Usable? An Empirical Study of Ownership, Assets, and Typestate in ObsidianOOPSLA
Posters
Michael Coblenz University of Maryland at College Park, Jonathan Aldrich Carnegie Mellon University, Brad A. Myers Carnegie Mellon University, Joshua Sunshine Carnegie Mellon University
08:20
40m
Poster
Multiparty Session Programming with Global Protocol CombinatorsECOOP
Posters
Keigo Imai Gifu University, Rumyana Neykova Brunel University London, Nobuko Yoshida Imperial College London, Shoji Yuen Nagoya University
08:20
40m
Poster
Static Race Detection and Mutex Safety and Liveness for Go ProgramsECOOP
Posters
Julia Gabet Imperial College London, Nobuko Yoshida Imperial College London
08:20
40m
Poster
CAMP: Cost-Aware Multiparty Session ProtocolsOOPSLA
Posters
David Castro-Perez Imperial College London, Nobuko Yoshida Imperial College London
08:20
40m
Poster
A Case Study in Language-Based Security: Building an I/O Library for WyvernOnward! Papers
Posters
Jennifer Fish Carnegie Mellon University, Darya Melicher Google, Jonathan Aldrich Carnegie Mellon University
08:20
40m
Poster
On the Unusual Effectiveness of Type-aware Operator Mutations for Testing SMT SolversOOPSLA
Posters
Dominik Winterer ETH Zurich, Chengyu Zhang East China Normal University, Zhendong Su ETH Zurich
08:20
40m
Poster
Reshape Your Layouts, Not Your Programs: A Safe Language Extension for Better Cache LocalityECOOP
Posters
Alexandros Tasos Imperial College London, Juliana Franco Microsoft Research, Cambridge, Sophia Drossopoulou Imperial College London, Tobias Wrigstad Uppsala University, Sweden, Susan Eisenbach Imperial College London
08:20
40m
Poster
A Type-Directed Operational Semantics for a Calculus with a Merge OperatorECOOP
Posters
Xuejing Huang The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
08:20
40m
Poster
Geometry Types for Graphics ProgrammingOOPSLA
Posters
Dietrich Geisler Cornell University, Irene Yoon University of Pennsylvania, Aditi Kabra Carnegie Mellon University, Horace He Cornell University, Yinnon Sanders Cornell University, Adrian Sampson Cornell University
20:20 - 21:00
Posters Session 1 MirrorPosters at SPLASH-VII
20:20
40m
Poster
Analogy-Making as a Core Primitive in the Software Engineering ToolboxOnward! Papers
Posters
Matthew Sotoudeh University of California, Davis, Aditya V. Thakur University of California, Davis
20:20
40m
Poster
Static Race Detection and Mutex Safety and Liveness for Go ProgramsECOOP
Posters
Julia Gabet Imperial College London, Nobuko Yoshida Imperial College London
20:20
40m
Poster
On the Unusual Effectiveness of Type-aware Operator Mutations for Testing SMT SolversOOPSLA
Posters
Dominik Winterer ETH Zurich, Chengyu Zhang East China Normal University, Zhendong Su ETH Zurich
20:20
40m
Poster
A Type-Directed Operational Semantics for a Calculus with a Merge OperatorECOOP
Posters
Xuejing Huang The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
20:20
40m
Poster
Knowing When to Ask: Sound Scheduling of Name Resolution in Type Checkers Derived from Declarative SpecificationsOOPSLA
Posters
Arjen Rouvoet Delft University of Technology, Hendrik van Antwerpen Delft University of Technology, Casper Bach Poulsen Delft University of Technology, Robbert Krebbers Radboud University Nijmegen, Eelco Visser Delft University of Technology
20:20
40m
Poster
A Case Study in Language-Based Security: Building an I/O Library for WyvernOnward! Papers
Posters
Jennifer Fish Carnegie Mellon University, Darya Melicher Google, Jonathan Aldrich Carnegie Mellon University
20:20
40m
Poster
CAMP: Cost-Aware Multiparty Session ProtocolsOOPSLA
Posters
David Castro-Perez Imperial College London, Nobuko Yoshida Imperial College London
20:20
40m
Poster
Owicki-Gries Reasoning for C11 RARECOOP
Posters
Sadegh Dalvandi University of Surrey, Simon Doherty University of Sheffield, Brijesh Dongol University of Surrey, Heike Wehrheim Paderborn University
20:20
40m
Poster
Formulog: Datalog for SMT-based Static AnalysisOOPSLA
Posters
Aaron Bembenek Harvard University, Michael Greenberg Pomona College, Stephen Chong Harvard University
20:20
40m
Poster
Demystifying DependenceOnward! Papers
Posters
20:20
40m
Poster
Row and Bounded Polymorphism via Disjoint PolymorphismECOOP
Posters
Ningning Xie The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong, Xuan Bi The University of Hong Kong, Tom Schrijvers KU Leuven
20:20
40m
Poster
Reshape Your Layouts, Not Your Programs: A Safe Language Extension for Better Cache LocalityECOOP
Posters
Alexandros Tasos Imperial College London, Juliana Franco Microsoft Research, Cambridge, Sophia Drossopoulou Imperial College London, Tobias Wrigstad Uppsala University, Sweden, Susan Eisenbach Imperial College London
20:20
40m
Poster
Gradual Verification of Recursive Heap Data StructuresOOPSLA
Posters
Jenna Wise (DiVincenzo) Carnegie Mellon University, Johannes Bader Jane Street, Cameron Wong Jane Street, Jonathan Aldrich Carnegie Mellon University, Éric Tanter University of Chile, Joshua Sunshine Carnegie Mellon University
20:20
40m
Poster
Multiparty Session Programming with Global Protocol CombinatorsECOOP
Posters
Keigo Imai Gifu University, Rumyana Neykova Brunel University London, Nobuko Yoshida Imperial College London, Shoji Yuen Nagoya University
20:20
40m
Poster
Can Advanced Type Systems Be Usable? An Empirical Study of Ownership, Assets, and Typestate in ObsidianOOPSLA
Posters
Michael Coblenz University of Maryland at College Park, Jonathan Aldrich Carnegie Mellon University, Brad A. Myers Carnegie Mellon University, Joshua Sunshine Carnegie Mellon University
20:20
40m
Poster
Geometry Types for Graphics ProgrammingOOPSLA
Posters
Dietrich Geisler Cornell University, Irene Yoon University of Pennsylvania, Aditi Kabra Carnegie Mellon University, Horace He Cornell University, Yinnon Sanders Cornell University, Adrian Sampson Cornell University