SPLASH 2021 (series) / HATRA 2021 (series) / Human Aspects of Types and Reasoning Assistants /
Towards an Incremental Dataset of Proofs
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.
Tue 19 OctDisplayed time zone: Central Time (US & Canada) change
Tue 19 Oct
Displayed time zone: Central Time (US & Canada) change
13:50 - 15:10 | |||
13:50 15mTalk | 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 15mTalk | Towards an Incremental Dataset of Proofs HATRA Hanneli Tavante McGill University Pre-print | ||
14:20 15mTalk | 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 15mTalk | 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 20mTalk | Paper discussion, session 2 HATRA | ||
