论文标题
检查您的（学生）的证明与孔
Check Your (Students') Proofs-With Holes
论文作者
论文摘要
CYP（检查您的证明）（Durner and Noschinski 2013; Traytel 2019）验证了有关Haskell类似程序的证据。我们将CYP扩展到了用于程序和证明术语以及类型检查器的模式匹配器。 这允许使用CYP进行自动分级练习，在该练习中，目标是完成教师部分给出的程序和证明，作为孔。由于这允许程序中的漏洞，因此类型检查变得至关重要。以前，CYP假设该程序是由类型正确的讲师编写的，因此省略了对证明的类型检查。 CYP优雅地处理不完整的学生提交。它暂时接受孔，并完全检查完整的子树。 我们提出了基本的设计决策，对实施做出了一些评论，并包括了最近的课程中使用CYP作为莱比锡自动工具自动分级系统的一部分的示例练习。
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.
