检查你的（学生的）证明-有洞
Check Your (Students') Proofs-With Holes
摘要：
Cyp（Check Your Proofs）（Durner and Noschinski 2013; Traytel 2019）验证了Haskell类程序的证明。我们扩展了Cyp的模式匹配程序和证明条款，和类型检查器。这允许使用Cyp进行自动评分练习，其目标是完成部分由教师给出的程序和证明，作为带有漏洞的术语。由于这允许程序中存在漏洞，类型检查变得必不可少。以前，Cyp假设程序是由一个类型正确的指导者编写的，因此省略了证明的类型检查。Cyp优雅地处理不完整的学生提交。它暂时接受洞，并完全检查完整的子树。我们提出了基本的设计决策，对实施进行了一些评论，并包括最近使用Cyp作为莱比锡Autotool自动评分系统的一部分的课程的示例练习。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
