Teaching Induction with Functional Programming and A Proof Assistant
Peter-Michael Osera, Steve Zdancewic · 2013
Mathematical induction is a difficult subject for beginning students of computer science to fully grasp. In this short paper, we propose using functional programming and proof assistants as an aide in teaching mathematical induction in a traditional discrete mathemat-ics course. To demonstrate this approach, we created a proof-of-concept web-based tutorial on induction. In this tutorial, students write small functional programs and prove simple properties about them using inductive reasoning. The functional programming lan-guage is deliberately designed to be minimalistic so that it can be picked up quickly, especially if the student is already familiar with a functional programming language, and not be a distraction to the ultimate goal of learning induction. Furthermore, the tutorial fea-tures an online IDE for entering programs and proofs to minimize the barrier to entry for students and instructors. 1.