Computer Science | Grinnell College

Thursday, November 17, 2016
4:15 p.m. in Science 3821
Refreshments at 4:00 p.m. in the Computer Science Commons (Science 3817)

Sooji Son, ’18, Medha Gopalaswamy ’18 and Jianting Chen ’18 will present "ORC²A Proof Assistant."

There is a natural correspondence between mathematical proofs and computer programs. For instance, a recursive function and its correctness relate directly to inductive proofs in mathematics. However, many undergraduate students feel that there is a disconnect between the required mathematics and computer science curricula. There are several proof assistant tools which have been used by the educational community to introduce such concepts to students, but since these tools are not primarily created for educational purposes, students often do not benefit from them to the expected extent.

We have created an educational tool that draws from the benefits of existing provers and assistants and includes a novel proof language that mimics handwritten proofs. By creating a proof assistant targeted towards introductory computer science students with an intuitive user interface and a rich mechanism for providing constructive feedback, we hope to bridge the gap that many students find between mathematical proofs and program correctness.

Reilly Grant ’18 and Zachary Segall ’18 will present "Semi-Automated Program Synthesis."

Program synthesizers have evolved over the past several decades as a method for generating programs from user specifications. One approach to synthesis is using a type theoretic approach and proof search; the Myth synthesis engine uses this approach. One major difficulty with this synthesis model is the exponential blow up of the search space. To circumvent this issue, we present the Scout synthesis engine, designed for semi-automated synthesis: we expect that the user will be able to prune the search space more intelligently than a fully automatic synthesizer. Our study reveals limitations, advantages, and possible expansions of semi-automated program synthesis.