Autograder for Functional Programming and Beyond
summary
Automated grader proves functional students correct by checking program equivalence against teacher references using the Stainless verification system and SMT solvers, generating functional induction proofs and counterexamples when disproved. It matches functions by type directed and test directed search, merges equivalent calls, and runs a clustering algorithm across hundreds of submissions (400+ in classes, benchmarks up to 800) achieving over 90% classification on many exercises while some complex or timeout cases remain.
AI-written summary · about
chapters (12)
- 0:00Start
- 1:51Functional Programming: CS-210
- 7:12Why would students in an introductory course care about proofs?
- 8:57Why equivalence checking?
- 10:50Stainless
- 13:31Pairwise Equivalence Checking: An Example
- 17:18Function Call Matching: Solution
- 18:05Function Call Matching: An Example
- 19:11Function Call Matching: Type- and Test-Directed Search
- 22:33Clustering Algorithm: Illustration
- 24:05Clustering Algorithm: Bridges
- 36:11skills matter
related talks
30mFormal verification of Scala programs with Stainless
46mTesting in the world of Functional Programming
48mFunctional Programming
15mGrammar-Based Testing for Little Languages: An Experience Report with Student Compilers
51mWhen Types are Not Enough
47mProperty-Based Testing
43m(Programs), Proofs and Refutations (and Tests and Mutants)
16mSoftware Model Checking via Summary-Guided Search