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.

At 4:15 on Thursday, April 8, in Noyce 3821, Dr. Dan Garcia of the University of California - Berkeley will give a talk on his experience with a technological and pedagogical innovation:

When lecturing to a large class, one typically hears from a few, vocal participants, it's difficult to keep short-attention-span students engaged, there's no way to get high-resolution feedback, and there's no in-class learning community. Peer instruction with clickers addresses all these issues, and has been used in many classes at UC Berkeley with great success. We will share our experience using this technique for five years in a two-hundred-student sophomore computer-science class.

Refreshments will be served at 4:15 p.m. in the Computer Science Commons (Noyce 3817). The talk, Keeping the millennials engaged with active learning, will follow at 4:30 p.m. in Noyce 3821. Everyone is welcome to attend!