Bookmark and Share

Department of

Mathematics and Computer Science

Title

Programming with Equality

Event Start DateTuesday, February 14, 2012
Serra Hall, Room 101B
Event Start Time12:20 pm - 1:50 pm
CostCost: free
Message

Programming with Equality
Presented by Professor Mike Shulman, University of California, San Diego

Lunch will be provided.

Audience: students and faculty

Abstract
Mathematics and computer science are on the threshold of a unifying revolution, made necessary by two growing problems. On the one hand, mathematics has seen the advent of proofs (such as the Four-Color Theorem) which are too long for humans to read, thus requiring a computer to construct and verify. On the other hand, our dependence on increasingly complex software means we require assurances that that software is correct, which can only be supplied by mathematical proof. Amazingly, the routes to solving these two problems are the same: realizing that "proving" and "programming" are, essentially, the same activity.

In this talk we'll explore one thread of this unification, which starts by thinking of "proof by induction" in algorithmic terms. This leads us to view fundamental mathematical concepts as programming datatypes, making them accessible to computers. We'll focus particularly on the notion of "equality": what does it mean to say that two things are the same? It turns out that we can actually "define" equality, in a language which a computer can understand and manipulate. This provides a starting point for the computerization of mathematics and the mathematicization of computers.

ContactAmy Prout | aprout@sandiego.edu | 619-260-4706