Check Your (Students') Proofs-With Holes

TL;DR

This paper extends the Cyp proof verification system to handle incomplete student submissions with holes in programs and proofs, incorporating pattern matching and type checking to enable effective auto-grading of partially completed exercises.

Contribution

It introduces pattern matching and type checking into Cyp, allowing it to verify and grade incomplete student programs with holes, a feature not present in prior versions.

Findings

Cyp can now handle holes in programs and proofs.

The extended system supports auto-grading of partially completed exercises.

Implementation details and example exercises demonstrate practical usability.

Abstract

Cyp (Check Your Proofs) (Durner and Noschinski 2013; Traytel 2019) verifies proofs about Haskell-like programs. We extended Cyp with a pattern matcher for programs and proof terms, and a type checker. This allows to use Cyp for auto-grading exercises where the goal is to complete programs and proofs that are partially given by the instructor, as terms with holes. Since this allows holes in programs, type-checking becomes essential. Before, Cyp assumed that the program was written by a type-correct instructor, and therefore omitted type-checking of proofs. Cyp gracefully handles incomplete student submissions. It accepts holes temporarily, and checks complete subtrees fully. We present basic design decisions, make some remarks on implementation, and include example exercises from a recent course that used Cyp as part of the Leipzig Autotool auto-grading system.