SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Wed 7 Dec 2022 11:30 - 12:00 at Seminar Room G145 - In-Person Talks Chair(s): Jonathan Aldrich

Research on reasoning assistants tends to focus on interactive theorem provers that can mechanically verify fully formalized, rigorous proofs. In practice, however, little mathematics is formalized to such a degree. Instead, proof is treated as a social process, meant to convince and communicate an argument or insight to other human mathematicians. This extended abstract surveys work on weak reasoning assistants, i.e., tools that assist mathematicians in that social task without requiring a fully mechanized proof.

Wed 7 Dec

Displayed time zone: Auckland, Wellington change

10:30 - 12:00
In-Person TalksHATRA at Seminar Room G145
Chair(s): Jonathan Aldrich Carnegie Mellon University
10:30
30m
Talk
Exploring the Verifiability of Code Generated by GitHub Copilot
HATRA
Dakota Wong University of Waterloo, Austin Kothig University of Waterloo, Patrick Lam University of Waterloo
Link to publication
11:00
30m
Talk
Holbert: Reading, Writing, Proving and Learning in the Browser
HATRA
Liam O'Connor University of Edinburgh, Rayhana Amjad The University of Edinburgh
Link to publication Media Attached
11:30
30m
Talk
A Survey of Weak Reasoning Assistants
HATRA
Matthew Sotoudeh Stanford University
Link to publication