SPLASH 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States

This program is tentative and subject to change.

Tue 19 Oct 2021 14:05 - 14:20 at Zurich E - Types, Proofs, and Design Theory Chair(s): Alan Jeffrey

In this work, we describe an approach for a data-centered user study for proof assistant tools, targeting jsCoq. While we were not yet able to obtain an initial dataset from students enrolled in a Programming Languages course for Fall 2021, we report several hypothesis that could be validated upon the analysis of this data. Up to this point, there are no records of user studies involving large amounts of data for none of the existing tools. An analysis centered on user data could improve the overall usability of these interfaces by revealing issues with their design. In the educational field, the investigation could also help lecturers and staff to understand the students’ struggles and issues when learning Coq.

This program is tentative and subject to change.

Tue 19 Oct

Displayed time zone: Central Time (US & Canada) change

13:50 - 15:10
Types, Proofs, and Design TheoryHATRA at Zurich E
Chair(s): Alan Jeffrey Roblox
13:50
15m
Talk
Toward a Theory of Programming Language and Reasoning Assistant Design: Minimizing Cognitive Load
HATRA
Michael Coblenz University of Maryland at College Park
Link to publication
14:05
15m
Talk
Towards an Incremental Dataset of Proofs
HATRA
Hanneli Tavante McGill University
Pre-print
14:20
15m
Talk
Toward Hole-Driven Development with Liquid Haskell
HATRA
Patrick Redmond University of California at Santa Cruz, Gan Shen University of California, Santa Cruz, USA, Lindsey Kuper University of California at Santa Cruz
Link to publication
14:35
15m
Talk
Toward SMT-Based Refinement Types in Agda
HATRA
Gan Shen University of California, Santa Cruz, USA, Lindsey Kuper University of California at Santa Cruz
Link to publication
14:50
20m
Talk
Paper discussion, session 2
HATRA