Human Aspects of Types and Reasoning AssistantsHATRA 2020
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.
Wed 18 Nov Times are displayed in time zone: Central Time (US & Canada) change
00:20 - 01:00: Breakfast in ParisStudent Research Competition at SPLASH-I
| |||
00:20 - 01:00 Poster | Student Research Competition Student Research Competition |
02:20 - 03:00 Social Event | Meet The Speakers Meet The Speakers (MTS) |
04:20 - 05:00 Social Event | Meet The Speakers Meet The Speakers (MTS) |
06:20 - 07:00 Social Event | Meet The Speakers Meet The Speakers (MTS) |
08:20 - 09:00 Other | Awards Session Awards |
09:00 - 10:20 Keynote | Models and Programs: Better Togethersupported by Futurewei Keynotes Sriram RajamaniMicrosoft Research Link to publication |
10:20 - 11:00 Social Event | Meet The Speakers Meet The Speakers (MTS) |
11:00 - 12:20: Formal MethodsHATRA at SPLASH-IV Chair(s): Michael CoblenzUniversity of Maryland at College Park | |||
11:00 - 11:20 Meeting | Welcome and Introductions HATRA | ||
11:20 - 11:40 Talk | Towards user-friendliness in proof assistants: automated strategies algebraic effects and handlers HATRA April GonçalvesMetastate AG Pre-print | ||
11:40 - 12:00 Talk | Towards making formal methods normal: meeting developers where they are HATRA Alastair ReidArm Ltd, Luke ChurchUniversity of Cambridge, Shaked FlurGoogle Research, Sarah de HaasGoogle Research, Maritza JohnsonGoogle Research, Ben LaurieGoogle Research Link to publication |
12:20 - 13:00 Social Event | Meet The Speakers Meet The Speakers (MTS) |
13:00 - 13:20 Talk | The Usability of Ownership HATRA Will CrichtonStanford University Link to publication | ||
13:20 - 13:40 Talk | RustViz: Interactively Visualizing Ownership and Borrowing HATRA Gongming (Gabriel) LuoUniversity of Michigan, Vishnu ReddyUniversity of Michigan, Marcelo AlmeidaUniversity of Michigan, Yingying ZhuUniversity of Michigan, Ke DuUniversity of Michigan, Cyrus OmarUniversity of Michigan Link to publication Pre-print | ||
13:40 - 14:00 Talk | Guiding user annotations for units-of-measure verification HATRA Dominic OrchardUniversity of Kent, UK, Mistral ContrastinFacebook London, Matthew DanishUniversity of Cambridge, UK, Andrew RiceUniversity of Cambridge, UK Link to publication |
14:20 - 15:00 Social Event | Meet The Speakers Meet The Speakers (MTS) |
15:00 - 15:20 Talk | Programming languages shouldn't and needn't be Turing complete HATRA Pre-print | ||
15:20 - 15:40 Talk | User-Centered Programming Language Design: A Course-Based Case Study HATRA Michael CoblenzUniversity of Maryland at College Park, Ariel DavisCarnegie Mellon University, Megan HofmannCarnegie Mellon University, Vivian HuangCarnegie Mellon University, Siyue JinCarnegie Mellon University, Max Krieger, Kyle LiangCarnegie Mellon University, Brian WeiCarnegie Mellon University, Mengchen Sam YongCarnegie Mellon University, Jonathan AldrichCarnegie Mellon University Link to publication | ||
15:40 - 16:00 Meeting | Day 1 Discussion HATRA |
16:20 - 17:00 Social Event | Meet The Speakers Meet The Speakers (MTS) |
18:20 - 19:00 Social Event | Meet The Speakers Meet The Speakers (MTS) |
20:20 - 21:00 Other | Awards Session Awards |
21:00 - 22:20 Keynote | Models and Programs: Better Togethersupported by Futurewei Keynotes Sriram RajamaniMicrosoft Research Link to publication |
22:20 - 23:00 Social Event | Meet The Speakers Meet The Speakers (MTS) |
Thu 19 Nov Times are displayed in time zone: Central Time (US & Canada) change
00:20 - 01:00 Social Event | Meet The Speakers Meet The Speakers (MTS) |
02:20 - 03:00 Social Event | Meet The Speakers Meet The Speakers (MTS) |
04:20 - 05:00 Social Event | Meet The Speakers Meet The Speakers (MTS) |
06:20 - 07:00 Social Event | Meet The Speakers Meet The Speakers (MTS) |
07:00 - 08:20 Keynote | Why Digital Agriculture is Fertile Ground for Software Systems Researchsupported by IBM Research Keynotes Vikram S. AdveUniversity of Illinois at Urbana-Champaign Link to publication |
08:20 - 09:00 Social Event | Meet The Speakers Meet The Speakers (MTS) |
10:20 - 11:00 Social Event | Meet The Speakers Meet The Speakers (MTS) |
11:00 - 12:20 Poster | Student Research Competition Student Research Competition |
12:20 - 13:00 Social Event | Meet The Speakers Meet The Speakers (MTS) |
13:00 - 14:20: Novices and Application DomainsHATRA at SPLASH-VI Chair(s): Luke ChurchUniversity of Cambridge | |||
13:00 - 13:20 Talk | Model-Driven Synthesis for Programming Tutors HATRA Link to publication | ||
13:20 - 13:40 Talk | Towards Solver-Aided Creativity HATRA Chris MartensNorth Carolina State University Pre-print | ||
13:40 - 14:00 Talk | Opportunities and Challenges for Circuit Board Level Hardware Description Languages HATRA Link to publication Pre-print | ||
14:00 - 14:20 Talk | Hazel Tutor: Guiding Novices Through Type-Driven Development Strategies HATRA Pre-print |
14:20 - 15:00 Social Event | Meet The Speakers Meet The Speakers (MTS) |
15:00 - 16:20: Research Agenda PlanningHATRA at SPLASH-VI Chair(s): Michael CoblenzUniversity of Maryland at College Park | |||
15:00 - 16:20 Meeting | Research Agenda Planning HATRA |
16:20 - 17:00 Social Event | Meet The Speakers Meet The Speakers (MTS) |
18:20 - 19:00 Social Event | Meet The Speakers Meet The Speakers (MTS) |
19:00 - 20:20 Keynote | Why Digital Agriculture is Fertile Ground for Software Systems Researchsupported by IBM Research Keynotes Vikram S. AdveUniversity of Illinois at Urbana-Champaign Link to publication |
20:20 - 21:00 Social Event | Meet The Speakers Meet The Speakers (MTS) |
22:20 - 23:00 Social Event | Meet The Speakers Meet The Speakers (MTS) |
Call for Papers
HATRA welcomes two kinds of submissions:
- Extended abstracts summarizing existing published work that would be of interest to the community.
- 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