SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference

Programming language designers seek to provide strong tools to help developers reason about their programs. For example, the formal methods community seeks to enable developers to prove correctness properties of their code, and type system designers seek to exclude classes of undesirable behavior from programs. The security community creates tools to help developers achieve their security goals. In order to make these approaches as effective as possible for developers, recent work has integrated approaches from human-computer interaction research into programming language design. This workshop brings together programming languages, software engineering, security, and human-computer interaction researchers to investigate methods for making languages that provide stronger safety properties more effective for programmers and software engineers.

We have two goals: (1) to identify and establish a research agenda for collaborative work in this space; (2) to provide a venue for discussion and feedback on early-stage approaches that might enable people to be more effective at achieving stronger safety properties in their programs.

HATRA is interested in two different kinds of contributions. First, extended abstracts that summarize an existing body of work that is relevant to the workshop’s topic; the presentations serve to familiarize the community, which may be diverse, with work that already exists. Second, research papers that describe a new idea, approach, or hypothesis in the space, and are presented as an opportunity for the authors to receive community feedback and for the community to seek inspiration from others.

The day will be divided into three segments. In the first segment, authors of accepted extended abstracts will present their work in approximately 20-minute time slots, followed by 10 minutes of discussion. To promote discussion, participants will be divided into small groups; then, the whole group will re-convene to discuss high-level points that arose in the small group discussions. In the second segment, authors of accepted papers will present their work. Then, in the third segment, we will conduct an activity to identify interesting research questions and help the community establish a research agenda. The organizers will produce a report after the workshop that catalogs the resulting agenda.

Dates
Plenary
You're viewing the program in a time zone which is different from your device's time zone change time zone

Wed 18 Nov

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

00:20 - 01:00
Breakfast in ParisStudent Research Competition at SPLASH-I
  • Aidan Yang, SOAR: Synthesis for Open-Source API Refactoring

  • Gahwon Lee, SASIL: A Domain-Specific Language for Simulating Declarative Specifications of Scheduling Systems

  • Ian C. McCormack, A Software Library Model for the Internet of Things

  • Mona Zhang and Jacob Gorenburg, Design and Implementation of a Gradual Verifier

  • Raphael Mosaner, Machine Learning to Ease Understanding of Data Driven Compiler Optimizations

  • Reed Oei, Psamathe: A DSL for Safe Blockchain Assets

  • Sang Heon Choi, Consolidation: A Technique for Improving Permissiveness of Human-Machine Interfaces

  • Sophia Kolak, Detecting Performance Patterns with Deep Learning

  • Vitaly Romanov, Evaluating Importance of Edge Types when Using Graph Neural Network for Predicting Return Types of Python Functions

00:20
40m
Poster
Student Research Competition
Student Research Competition

02:20 - 03:00
Cocktails in SydneyMeet The Speakers (MTS) at SPLASH-I
02:20
40m
Social Event
Meet The Speakers
Meet The Speakers (MTS)

04:20 - 05:00
Dinner in BejingMeet The Speakers (MTS) at SPLASH-I
04:20
40m
Social Event
Meet The Speakers
Meet The Speakers (MTS)

06:20 - 07:00
06:20
40m
Social Event
Meet The Speakers
Meet The Speakers (MTS)

08:20 - 09:00
Breakfast in ChicagoAwards at SPLASH-I +12h
08:20
40m
Other
Awards Session
Awards
David Grove IBM Research, Jens Palsberg University of California, Los Angeles
09:00 - 10:20
WKeynotes at SPLASH-I +12h
Chair(s): Hridesh Rajan Iowa State University, USA
09:00
80m
Keynote
Models and Programs: Better Togethersupported by Futurewei
Keynotes
Sriram Rajamani Microsoft Research
Link to publication
10:20 - 11:00
Breakfast in SeattleMeet The Speakers (MTS) at SPLASH-I +12h
10:20
40m
Social Event
Meet The Speakers
Meet The Speakers (MTS)

11:00 - 12:20
Formal MethodsHATRA at SPLASH-IV
Chair(s): Michael Coblenz University of Maryland at College Park
11:00
20m
Meeting
Welcome and Introductions
HATRA

11:20
20m
Talk
Towards user-friendliness in proof assistants: automated strategies algebraic effects and handlers
HATRA
April Gonçalves Metastate AG
Pre-print
11:40
20m
Talk
Towards making formal methods normal: meeting developers where they are
HATRA
Alastair Reid Arm Ltd, Luke Church University of Cambridge, Shaked Flur Google Research, Sarah de Haas Google Research, Maritza Johnson Google Research, Ben Laurie Google Research
Link to publication
12:20 - 13:00
Breakfast in WellingtonMeet The Speakers (MTS) at SPLASH-I +12h
12:20
40m
Social Event
Meet The Speakers
Meet The Speakers (MTS)

13:00 - 14:20
TypesHATRA at SPLASH-IV
Chair(s): Peter-Michael Osera Grinnell College
13:00
20m
Talk
The Usability of Ownership
HATRA
Will Crichton Stanford University
Link to publication
13:20
20m
Talk
RustViz: Interactively Visualizing Ownership and Borrowing
HATRA
Gongming (Gabriel) Luo University of Michigan, Vishnu Reddy University of Michigan, Marcelo Almeida University of Michigan, Yingying Zhu University of Michigan, Ke Du University of Michigan, Cyrus Omar University of Michigan
Link to publication Pre-print
13:40
20m
Talk
Guiding user annotations for units-of-measure verification
HATRA
Dominic Orchard University of Kent, UK, Mistral Contrastin Facebook London, Matthew Danish University of Cambridge, UK, Andrew Rice University of Cambridge, UK
Link to publication
14:20 - 15:00
Cocktails in ParisMeet The Speakers (MTS) at SPLASH-I +12h
14:20
40m
Social Event
Meet The Speakers
Meet The Speakers (MTS)

15:00 - 16:20
DesignHATRA at SPLASH-IV
Chair(s): Luke Church University of Cambridge
15:00
20m
Talk
Programming languages shouldn't and needn't be Turing complete
HATRA
Pre-print
15:20
20m
Talk
User-Centered Programming Language Design: A Course-Based Case Study
HATRA
Michael Coblenz University of Maryland at College Park, Ariel Davis Carnegie Mellon University, Megan Hofmann Carnegie Mellon University, Vivian Huang Carnegie Mellon University, Siyue Jin Carnegie Mellon University, Max Krieger , Kyle Liang Carnegie Mellon University, Brian Wei Carnegie Mellon University, Mengchen Sam Yong Carnegie Mellon University, Jonathan Aldrich Carnegie Mellon University
Link to publication
15:40
20m
Meeting
Day 1 Discussion
HATRA

16:20 - 17:00
Breakfast in SeoulMeet The Speakers (MTS) at SPLASH-I +12h
16:20
40m
Social Event
Meet The Speakers
Meet The Speakers (MTS)

18:20 - 19:00
Cocktails in RioMeet The Speakers (MTS) at SPLASH-I +12h
18:20
40m
Social Event
Meet The Speakers
Meet The Speakers (MTS)

20:20 - 21:00
Cocktails in New YorkAwards at SPLASH-I
20:20
40m
Other
Awards Session
Awards
David Grove IBM Research, Jens Palsberg University of California, Los Angeles
21:00 - 22:20
WKeynotes at SPLASH-I
Chair(s): Hridesh Rajan Iowa State University, USA
21:00
80m
Keynote
Models and Programs: Better Togethersupported by Futurewei
Keynotes
Sriram Rajamani Microsoft Research
Link to publication
22:20 - 23:00
22:20
40m
Social Event
Meet The Speakers
Meet The Speakers (MTS)

Thu 19 Nov

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

00:20 - 01:00
Breakfast in ParisMeet The Speakers (MTS) at SPLASH-I
00:20
40m
Social Event
Meet The Speakers
Meet The Speakers (MTS)

02:20 - 03:00
Cocktails in SydneyMeet The Speakers (MTS) at SPLASH-I
02:20
40m
Social Event
Meet The Speakers
Meet The Speakers (MTS)

04:20 - 05:00
Dinner in BeijingMeet The Speakers (MTS) at SPLASH-I
04:20
40m
Social Event
Meet The Speakers
Meet The Speakers (MTS)

06:20 - 07:00
06:20
40m
Social Event
Meet The Speakers
Meet The Speakers (MTS)

07:00 - 08:20
RKeynotes at SPLASH-I +12h
Chair(s): David Grove IBM Research
07:00
80m
Keynote
Why Digital Agriculture is Fertile Ground for Software Systems Researchsupported by IBM Research
Keynotes
Vikram S. Adve University of Illinois at Urbana-Champaign
Link to publication
08:20 - 09:00
Breakfast in ChicagoMeet The Speakers (MTS) at SPLASH-I +12h
08:20
40m
Social Event
Meet The Speakers
Meet The Speakers (MTS)

10:20 - 11:00
Breakfast in SeattleMeet The Speakers (MTS) at SPLASH-I +12h
10:20
40m
Social Event
Meet The Speakers
Meet The Speakers (MTS)

11:00 - 12:20
11:00
80m
Poster
Student Research Competition
Student Research Competition

12:20 - 13:00
Breakfast in WellingtonMeet The Speakers (MTS) at SPLASH-I +12h
12:20
40m
Social Event
Meet The Speakers
Meet The Speakers (MTS)

13:00 - 14:20
Novices and Application DomainsHATRA at SPLASH-VI
Chair(s): Luke Church University of Cambridge
13:00
20m
Talk
Model-Driven Synthesis for Programming Tutors
HATRA
Niek Mulleners Utrecht University, Johan Jeuring Open University of the Netherlands, Netherlands
Link to publication
13:20
20m
Talk
Towards Solver-Aided Creativity
HATRA
Chris Martens North Carolina State University
Pre-print
13:40
20m
Talk
Opportunities and Challenges for Circuit Board Level Hardware Description Languages
HATRA
Richard Lin University of California, Berkeley, Bjoern Hartmann UC Berkeley
Link to publication Pre-print
14:00
20m
Talk
Hazel Tutor: Guiding Novices Through Type-Driven Development Strategies
HATRA
Hannah Potter University of Michigan, Cyrus Omar University of Michigan
Pre-print
14:20 - 15:00
Cocktails in ParisMeet The Speakers (MTS) at SPLASH-I +12h
14:20
40m
Social Event
Meet The Speakers
Meet The Speakers (MTS)

15:00 - 16:20
Research Agenda PlanningHATRA at SPLASH-VI
Chair(s): Michael Coblenz University of Maryland at College Park
15:00
80m
Meeting
Research Agenda Planning
HATRA

16:20 - 17:00
Breakfast in SeoulMeet The Speakers (MTS) at SPLASH-I +12h
16:20
40m
Social Event
Meet The Speakers
Meet The Speakers (MTS)

18:20 - 19:00
Cocktails in RioMeet The Speakers (MTS) at SPLASH-I +12h
18:20
40m
Social Event
Meet The Speakers
Meet The Speakers (MTS)

19:00 - 20:20
RKeynotes at SPLASH-I
Chair(s): David Grove IBM Research
19:00
80m
Keynote
Why Digital Agriculture is Fertile Ground for Software Systems Researchsupported by IBM Research
Keynotes
Vikram S. Adve University of Illinois at Urbana-Champaign
Link to publication
20:20 - 21:00
Cocktails in New YorkMeet The Speakers (MTS) at SPLASH-I
20:20
40m
Social Event
Meet The Speakers
Meet The Speakers (MTS)

22:20 - 23:00
22:20
40m
Social Event
Meet The Speakers
Meet The Speakers (MTS)

Call for Papers

HATRA welcomes two kinds of submissions:

  1. Extended abstracts summarizing existing published work that would be of interest to the community.
  2. Research proposals, position papers, and early-stage result papers. These come in short (up to four pages) and long (up to eight pages) varieties. These may describe hypotheses, ideas for research, or early-stage results. The objective is to provide an opportunity for the authors to receive feedback from the community as well as to help inspire participants to identify and clarify their own research directions. To encourage submission of ideas that may be published in other venues in the future, papers will not be published in the ACM Digital Library.

Topics of interest include, but are not limited to:

  • Type system design
  • Programming language evaluation
  • Programming language and tool design methodology
  • Interactive theorem provers
  • Lightweight specification tools
  • Proof engineering
  • Psychology of programming

HATRA will use a review process that is optionally double-blind. Ideally, authors should omit identifying information from their papers, and should reference their own related work in the third person. However, if this is impractical, perhaps because you are submitting an extended abstract, you may include author information in your submission.

Extended abstracts may be in either one-page “sigconf” format or two-page “ACM Small” format. Other submissions should be in “ACM Small” style. Papers should be submitted using HotCRP by September 18, 2020: https://hatra20.hotcrp.com