Sun 14 Jun 2015 16:40 - 17:20 at C120-C121 - Session4

With the rise of MOOCs, much attention has been paid to how programming language technology can help facilitate programming education. This has taken many forms, for example, automatic grading, generation of problems and feedback, and program execution visualization. However, for all of its close connections with programming, mathematical proof has not enjoyed the same level of automation and support. Students still write proofs by hand, and those proofs are hand-checked by a teacher and their TAs, a situation that clearly does not scale. Could we use programming language technology to help facilitate pedagogy around mathematical proof like we do with programming?

To explore this question, we are developing an online tutorial for mathematical proof by induction through functional programming called InductFun. Students develop functional programs in a restricted functional programming language and then prove properties about them directly in InductFun. The platform is backed by the Coq proof assistant.

In this talk, I present the current state of InductFun and discuss our on-going work in creating a tool that supports pedagogy around proofs. In particular, I discuss the design space surrounding InductFun where we balance the strength of a proof assistant with the needs of educators teaching proof in computer science courses.

Sun 14 Jun

16:00 - 18:00: PLOOC 2015 - Session4 at C120-C121
PLOOC-2015-papers16:00 - 16:40
Alex PolozovUniversity of Washington, Eleanor O'RourkeUniversity of Washington, Adam SmithUniversity of Washington, Luke ZettlemoyerUniversity of Washington, Sumit GulwaniMicrosoft Research, Zoran PopovicUniversity of Washington
PLOOC-2015-papers16:40 - 17:20
Peter-Michael OseraUniversity of Pennsylvania, Steve Zdancewic
PLOOC-2015-papers17:20 - 18:00
Elena GlassmanMIT, Jeremy ScottMIT, Rishabh SinghMicrosoft Research, Philip GuoUniversity of Rochester, Robert MillerMIT