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
Times are displayed in time zone: Tijuana, Baja California change

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