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

This paper presents Holbert, a work-in-progress pedagogical proof assistant and online textbook platform, aimed at the educational use-case, specifically for the teaching of programming language theory. Holbert allows proof exercises and rule definitions to be embedded directly in an online textbook, where proofs and rules can be manipulated using a graphical interface. We give an overview of the logical foundations of Holbert, examples of its use, and give an update as to its current implementation status.

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
Hide past events