ICFP 2021
Sun 22 - Sat 28 August 2021
Fri 27 Aug 2021 02:45 - 03:00 at ML - Inference + Short talks Chair(s): Ohad Kammar

In this talk, we describe an approach for a data-centered user study for proof assistant tools, targeting jsCoq. There is a wide variety of interfaces for Coq (in standalone formats, such as CoqIDE; as web resources, like jsCoq, and plugins for major IDEs). But 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 better when learning Coq. This talk shows a work in progress demo for a data collection procedure in jsCoq, and summarizes a few key discussion points for the educators involved in the Coq community.

Abstract (hanneli-ml21-submission.pdf)268KiB
Slides (ml21-hanneli.pdf)1.32MiB