Programming with Equality

Programming with Equality

Programming with Equality

This event occurred in the past

Date and Time

  • Tuesday, February 14, 2012 from 12:20 p.m. to 1:50 p.m.


Serra Hall, Room 101B

5998 Alcala Park San Diego, CA 92110




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

Lunch will be provided.

Audience: students and faculty

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.

Contact Us Email

Phone: (619) 260-4600
Fax: (619) 260-4162

Visit Campus Map

Founders Hall
5998 Alcalá Park
San Diego, CA 92110