2020/09/02 by Dennis Renz, Renz, Dennis, Sibylle Schwarz +3
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic, programming, and type systems #Programming Languages (cs.PL) #Teaching and Learning Programming
paper · pdf · doi:10.48550/arxiv.2009.01326
openalex publication_date 2020/09/02 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.