Human Aspects of Types and Reasoning Assistants (HATRA 2026)HATRA 2026

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. The 7th International Workshop on Human Aspects of Types and Reasoning Assistants 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 three 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. Finally, and new this year, we are soliciting tutorial/feedback session proposals in which tool creators teach participants how to use their tools and solicit design feedback.

The day will be divided into two segments. In the first segment, authors of accepted papers and tutorials 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 will be a hybrid workshop. Participants will be able to join and present in person or remotely.

Keynote Speaker

We are delighted to announce a keynote by Ravi Chugh. Prof. Chugh is a computer scientist at the University of Chicago whose research centers on Direct Manipulation Programming Systems — work aimed at making programming more interactive and tangible, like GUIs, while making GUIs more transparent and powerful, like programming. He has also contributed to work spanning program synthesis, type systems for scripting languages, and visualization tools.

Title: The Next 700 Block-Based Editors

Abstract: Block-based code editors have been adopted widely in classrooms with young learners, yet they are often perceived as inferior compared to the ultimate flexibility of text editors. Beyond blocks, alternatives to manipulating programs as text have been pursued through various structure-editing interfaces. But blocks, text, and structure-editing each have merits. Can’t we all just get along? This talk presents ongoing work which aims to integrate these complementary ways of reading, writing, and maintaining programs. The central element is a novel user interface primitive called ragged blocks (or rocks), which allow nested passages of structured text—like code—to be styled and rendered in ways that suggest alluring possibilities for future programming environments and other GUIs.

Accepted Papers

Call for Papers

New this year: tutorial feedback sessions!

HATRA welcomes three 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.
• Proposals for tutorials. These may be longer, more interactive presentations that demonstrate the use of a tool. These are reserved for tools that are mature enough that attendees can try using the tool themselves. Submissions should describe the tool that is to be shown and the kind of feedback that will be solicited from the audience.

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.

All submissions should pertain to the relationship between programming languages and developers who use those languages.

Topics of interest include, but are not limited to:

• Type system design
• Programming language evaluation
• Programming language and tool design methodology
• Interactive theorem provers and their usage
• 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 and tutorials 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).