Automatic Assessment and Feedback on Undergraduates' Structural Induction Proofs

Abstract. To help students learn the structural induction proof technique, we aim to provide a scalable approach to give immediate comprehensive feedback as well as a fair assessment for students’ proofs. To this end, we developed an automatic proof checking approach tailored for helpful feedback, a fair assessment schema for structural induction proofs, and an easy to learn DSL for tasks and solutions. We implemented Automatic Structural Induction Assessor (ASIA), a command line tool that automatically provides helpful feedback and awards points for a given solution. To evaluate our approach in practice, we employed ASIA in three undergraduate computer science courses (with around 60 students each) and conducted a questionnaire survey focusing on the tool’s usability, quality of the provided feedback and the student’s task load. We found that ASIA provided comprehensive feedback and a fair assessment for students, as well as limited manual reassessment for teachers. This repository provides the replication package, containing ASIA, featured exercises, as well as anonymized questionnaire and case study results.