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 |
Fri 27 AugDisplayed time zone: Seoul change
01:30 - 03:00 | |||
01:30 30mTalk | Frozen inference constraints for type-directed disambiguation ML Pre-print Media Attached | ||
02:00 15mTalk | Experience Report: Domain Modeling with F# (short talk) ML Scott Wlaschin None Media Attached File Attached | ||
02:15 15mTalk | Isomorphisms are back! (short talk) ML File Attached | ||
02:30 15mTalk | Sylvester: Unified, typed, notation for symbolic mathematics and proofs (short talk) ML Allister Beharry None Media Attached File Attached | ||
02:45 15mTalk | A Data-centered User Study for jsCoq (short talk) ML Hanneli Tavante McGill University File Attached |