SPLASH 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States

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.

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

Tue 19 Oct

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

10:50 - 12:10
Type SystemsHATRA at Zurich E
Chair(s): Chris Martens North Carolina State University
10:50
15m
Talk
Human Aspects of SASyLF, an Educational Proof Assistant for Type Theory
HATRA
Jonathan Aldrich Carnegie Mellon University
Pre-print
11:05
15m
Talk
An Empirical Study of Protocols in Smart Contracts
HATRA
Timothy Mou Swarthmore College, Michael Coblenz University of Maryland at College Park, Jonathan Aldrich Carnegie Mellon University
Link to publication
11:20
15m
Talk
Position Paper: Goals of the Luau Type System
HATRA
Lily Brown Roblox, Andy Friesen Roblox, Alan Jeffrey Roblox
Link to publication
11:35
15m
Talk
User-driven design and evaluation of Liquid Types in Java
HATRA
Catarina Gamboa LASIGE, Faculdade de Ciências da Universidade de Lisboa, Paulo Canelas LASIGE, Faculdade de Ciências da Universidade de Lisboa, Christopher Steven Timperley Carnegie Mellon University, Alcides Fonseca LASIGE, Faculdade de Ciências da Universidade de Lisboa
Pre-print
11:50
20m
Meeting
Paper discussion, session 1
HATRA

13:50 - 15:10
Types, Proofs, and Design TheoryHATRA at Zurich E
Chair(s): Alan Jeffrey Roblox
13:50
15m
Talk
Toward a Theory of Programming Language and Reasoning Assistant Design: Minimizing Cognitive Load
HATRA
Michael Coblenz University of Maryland at College Park
Link to publication
14:05
15m
Talk
Towards an Incremental Dataset of Proofs
HATRA
Hanneli Tavante McGill University
Pre-print
14:20
15m
Talk
Toward Hole-Driven Development with Liquid Haskell
HATRA
Patrick Redmond University of California at Santa Cruz, Gan Shen University of California, Santa Cruz, USA, Lindsey Kuper University of California at Santa Cruz
Link to publication
14:35
15m
Talk
Toward SMT-Based Refinement Types in Agda
HATRA
Gan Shen University of California, Santa Cruz, USA, Lindsey Kuper University of California at Santa Cruz
Link to publication
14:50
20m
Talk
Paper discussion, session 2
HATRA

15:40 - 17:00
Novel Interfaces and DiscussionHATRA at Zurich E
Chair(s): Jonathan Aldrich Carnegie Mellon University

First, authors will present two papers, and we will have 10 minutes to discuss them. Then, we will use the remaining 40 minutes for group discussion of promising research directions.

15:40
15m
Talk
Typed Image-based Programming with Structure Editing
HATRA
Jonathan Edwards , Tomas Petricek University of Kent
Link to publication
15:55
15m
Talk
A New Medium for Communicating Research on Programming Languages
HATRA
Will Crichton Stanford University
Pre-print
16:10
10m
Talk
Paper discussion, session 3
HATRA

16:20
40m
Meeting
General discussion
HATRA

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 plus unlimited references) and long (up to eight pages plus unlimited references) 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 August 6, 2021: https://hatra21.hotcrp.com

Questions? Use the HATRA contact form.