[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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 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
The submission deadline is August 6, 2021. For more information, please see the
web site: https://2021.splashcon.org/home/hatra-2021
<https://2021.splashcon.org/home/hatra-2021>
Organizing Committee:
Michael Coblenz (University of Maryland)
Luke Church (University of Cambridge)
Chris Martens (North Carolina State University)
Program Committee:
Will Crichton (Stanford University)
Jonathan Edwards
Molly Feldman (Williams College)
Andrew Head (UC Berkeley)
Alan Jeffrey (Roblox)
Shriram Krishnamurthi (Brown University)
Niek Mulleners (Utrecht University)
Cyrus Omar (University of Michigan)
Peter-Michael Osera (Grinnell College)
Hila Peleg (Technion Israel Institute of Technology)
Alastair Reid (Google Research)
Tianyi Zhang (Harvard University)
