SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal

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 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; (2) to facilitate discussion about relevant topics of participant interest.

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 two segments. In the first segment, authors of accepted papers will present their work. In the second segment, we will conduct an “unconference”-style meeting. By allowing the participants to drive the agenda, we hope to focus on topics that provide stimulating and enlightening discussion.

HATRA 2023 will be a hybrid workshop. Participants will be able to join and present in person or remotely.

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

Sun 22 Oct

Displayed time zone: Lisbon change

10:30 - 11:00
Coffee BreakCatering at Gallery
11:00 - 12:30
Formalisms and SynthesisHATRA at Room VI
Chair(s): Michael Coblenz University of California, San Diego
11:00
30m
Talk
Diagrammatic notations for interactive theorem proving
HATRA
Link to publication
11:30
30m
Talk
Exploratory Study on Multi-User Program Synthesis: A Multi-Wizard ApproachRemote
HATRA
Tyler Holloway Harvard University, Nada Amin Harvard University, Elena Glassman Harvard University
12:00
30m
Talk
Latte: Lightweight Aliasing Tracking for Java
HATRA
Conrad Zimmerman Brown University, Catarina Gamboa Carnegie Mellon University and LASIGE, University of Lisbon, Alcides Fonseca LASIGE, University of Lisbon, Jonathan Aldrich Carnegie Mellon University
Link to publication
12:30 - 14:00
14:00 - 15:30
Interactivity and Visualization for ProgrammersHATRA at Room VI
Chair(s): Jonathan Aldrich Carnegie Mellon University
14:00
30m
Talk
Debugging Trait Errors as Logic Programs
HATRA
Gavin Gray ETH Zurich, Will Crichton Brown University
Link to publication
14:30
30m
Talk
Totally Live Programming with Hazel (Progress Report)
HATRA
Cyrus Omar University of Michigan, Andrew Blinn University of Michigan, David Moon University of Michigan
Link to publication
15:00
30m
Talk
REVIS: An Error Visualization Tool for RustRemote
HATRA
Ruochen Wang University of California, San Diego, Molly MacLaren University of California, San Diego, Michael Coblenz University of California, San Diego
Link to publication
15:30 - 16:00
Coffee BreakCatering at Gallery
16:00 - 17:30
Type Systems and DiscussionHATRA at Room VI
Chair(s): Will Crichton Brown University
16:00
45m
Talk
Goals of the Luau Type System, Two Years OnRemote
HATRA
Lily Brown Roblox, Andy Friesen Roblox, Alan Jeffrey Roblox
Link to publication
16:45
45m
Meeting
Discussion
HATRA
Michael Coblenz University of California, San Diego, Luke Church University of Cambridge | Lund University | Lark Systems, Jonathan Aldrich Carnegie Mellon University, Will Crichton Brown University

Call for Papers

HATRA welcomes two kinds of submissions:

  • Extended abstracts (one page) summarizing existing published work that would be of interest to the community.
  • Research proposals, position papers, and early-stage result papers. Papers may be up to eight pages long, plus unlimited references. 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
  • Societal or social implications of programming languages and proof assistants

We request that papers be submitted anonymously when feasible. Extended abstracts are likely to include author names.

Papers should use the PACMPL templates (the same as the OOPSLA proceedings format: acmart-pacmpl-template.tex file with the acmsmall option).