SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Wed 18 Nov 2020 07:20 - 07:40 at SPLASH-I - W-1 Chair(s): Karim Ali, Sophia Drossopoulou
Wed 18 Nov 2020 19:20 - 19:40 at SPLASH-I - W-1 Chair(s): Patrick Lam, Julia Belyakova

Ensuring computations are unit-wise consistent is an important task in software development. Numeric computations are usually performed with primitive types instead of abstract data types, which results in very weak static guarantees about correct usage and conversion of units.
This paper presents PUnits, a pluggable type system for expressive units of measurement types and a precise, whole-program inference approach for these types. PUnits can be used in three modes: (1) modularly check the correctness of a program, (2) ensure a possible unit typing exists, and (3) annotate a program with units.
Annotation mode allows human inspection and is essential since having a valid typing does not guarantee that the inferred specification expresses design intent. PUnits is the first units type system with this capability.
Compared to prior work, PUnits strikes a novel balance between expressiveness, inference complexity, and annotation effort.
We implement PUnits for Java and evaluate it by specifying the correct usage of frequently used JDK methods.
We analyze 234k lines of code from eight open-source scientific computing projects with PUnits. We compare PUnits against an encapsulation-based units API (the javax.measure package) and discovered unit errors that the API failed to find. PUnits infers 90 scientific units for five of the projects and generates well-specified applications.
The experiments show that PUnits is an effective, sound, and scalable alternative to using encapsulation-based units APIs, enabling Java developers to reap the performance benefits of using primitive types instead of abstract data types for unit-wise consistent scientific computations.

Wed 18 Nov

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

07:00 - 08:20
W-1OOPSLA at SPLASH-I +12h
Chair(s): Karim Ali University of Alberta, Sophia Drossopoulou Imperial College London
07:00
20m
Talk
Mossad: Defeating Software Plagiarism Detection
OOPSLA
Breanna Devore-McDonald University of Massachusetts at Amherst, Emery D. Berger University of Massachusetts at Amherst
Link to publication DOI Media Attached
07:20
20m
Talk
Precise Inference of Expressive Units of Measurement Types
OOPSLA
Tongtong Xiang University of Waterloo, Jeff Y. Luo University of Waterloo, Werner Dietl University of Waterloo
Link to publication DOI Media Attached
07:40
20m
Talk
Program Equivalence for Assisted Grading of Functional Programs
OOPSLA
Joshua Clune Carnegie Mellon University, Vijay Ramamurthy Carnegie Mellon University, Ruben Martins Carnegie Mellon University, Umut A. Acar Carnegie Mellon University
Link to publication DOI Media Attached
08:00
20m
Talk
Revisiting Iso-Recursive Subtyping
OOPSLA
Yaoda Zhou University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong, Jinxu Zhao University of Hong Kong
Link to publication DOI Media Attached
19:00 - 20:20
W-1OOPSLA at SPLASH-I
Chair(s): Patrick Lam University of Waterloo, Julia Belyakova Northeastern University
19:00
20m
Talk
Mossad: Defeating Software Plagiarism Detection
OOPSLA
Breanna Devore-McDonald University of Massachusetts at Amherst, Emery D. Berger University of Massachusetts at Amherst
Link to publication DOI Media Attached
19:20
20m
Talk
Precise Inference of Expressive Units of Measurement Types
OOPSLA
Tongtong Xiang University of Waterloo, Jeff Y. Luo University of Waterloo, Werner Dietl University of Waterloo
Link to publication DOI Media Attached
19:40
20m
Talk
Program Equivalence for Assisted Grading of Functional Programs
OOPSLA
Joshua Clune Carnegie Mellon University, Vijay Ramamurthy Carnegie Mellon University, Ruben Martins Carnegie Mellon University, Umut A. Acar Carnegie Mellon University
Link to publication DOI Media Attached
20:00
20m
Talk
Revisiting Iso-Recursive Subtyping
OOPSLA
Yaoda Zhou University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong, Jinxu Zhao University of Hong Kong
Link to publication DOI Media Attached