SSS Abstracts  Fall 2008

Presented by James McCann, CSD

In my gradient-domain paint system, users specify color differences between pixels instead of (as in a traditional paint program) specifying pixel colors explicitly. While such a modality may at first seem unintuitive, it's actually quite easy to get the hang of -- in fact, given the way humans perceive color, it may make more sense than a traditional paint program!

In this talk I'll describe the work in graphics and perceptual psychology that led me to create such a program, the underlying technology (GPU-based multigrid) that keeps things running at interactive rates, and the brushes and blend modes that allow users to perform gradient-domain edits.

If you'd like to try out the paint system (and have a decent graphics card), visit http://gradient-paint.com where you can find binaries for Linux, OSX, and Windows as well as source code.

Squigl: A game for detecting objects in images

Friday, September 26^th, 2008 from 12-1 pm in Wean 5409.

Presented by Bryant Lee, CSD

We report on a fun web game we developed, called Squigl, where players label object locations for the purpose of training object detection algorithms. We explain how we deployed the game on a live gaming website and collected fifty thousand data points. We also perform a test by using some of the data in an actual object detection algorithm to see how it performs and how it compares with existing, state of the art databases for object detection. The results of the test showed that our data was as good as data collected from traditional methods. The contribution of this paper is a large and diverse dataset for training object detection algorithms and also the description of the successful methodology of using a web game to collect this data cheaply and easily. Using games to collect data has been applied previously, for example by the ESP Game, but Squigl represents a novel application to a broad area of AI not previously explored with this method.

Joint Work with: Luis von Ahn

Walking the way of duality (in programming)

Friday, October 10^th, 2008 from 12-1 pm in Wean 5409.

Presented by Noam Zeilberger, CSD

"So much time and so little to do. Wait a minute. Strike that. Reverse it." As Willy Wonka once observed, duality is a powerful tool for reorganizing old ideas, and for generating new ones. In this talk, I will explore ways in which duality can be used to give a simpler account of existing programming languages, as well as to build more expressive new languages. After reviewing some basic PL terminology such as "value", "continuation", "pattern-matching", and "evaluation order", I will explain how to view program evaluation abstractly as a game between two players: Valerie the value and Conor the continuation. This will lead us to discussing two different forms of duality. On the one hand, the players are dual in the sense that they must be able to respond to each other's moves (pattern-matching). On the other hand, there is a duality between games in which Valerie moves first, and games in which Conor moves first (evaluation order).

Finally, through the Curry-Howard correspondence, Valerie and Conor play the opposing roles of proof and refutation. In that case, the two forms of duality let us make sense of the ancient Aristotelian concept of the "square of opposition".

(In Partial Fulfillment of the Speaking Skills Requirement.)

Tale of Two Consequence Relations

Friday, October 17^th, 2008 from 12-1 pm in Wean 5409.

Presented by Dan Licata, CSD

A proof assistant is a tool for formalizing mathematics. In this talk, we will discuss proof assistants for reasoning about _deductive systems_ such as programming languages and proof theories. Such proof assistants are useful both for programming---e.g., implementing compilers and theorem provers---and for proving---e.g., formalizing the definition and properties of a programming language, or specifying and verifying software. To support these applications, proof assistants must provide means for (1) representing deductive systems and (2) programming and proving with them. Current proof assistants such as Twelf and Coq provide varying support for these tasks. A major part of this variation can be explained as a story about two _consequence relations_ called derivability and admissibility: Twelf makes it easy to use derivabilities in representations, whereas Coq provides no special support. On the other hand, Coq allows admissibilities to be used in representations, whereas Twelf does not. In this talk, we will explain the notions of derivability and admissibility, and discuss work on a new proof assistant that better integrates the two, combining the advantages of Twelf and Coq. This talk is based on joint work with Noam Zeilberger and Robert Harper, and is presented in partial fulfillment of the speaking requirement.

GOBLIN: A graphical model approach to computing free energies of protein structures

Friday, December 12^th, 2008 from 12-1 pm in Wean 5409.

Presented by Hetunandan Kamichetty, CSD

The behavior of a bio-molecular system is directly or indirectly governed by its free energy F. Computing F, is equivalent to computing the log partition function of a statistical ensemble.

I will present GOBLIN, a method of computing an approximation to F for protein structures, that models the statistical ensemble as an undirected graphical model and uses Generalized Belief Propagation on the graphical model to perform this approximation. I will also present results comparing the efficacy of GOBLIN with other putative approaches in predicting (changes to) F.

This talk will be geared at a general CS audience -- no prior biological knowledge will be needed.

Joint work with Chris Langmead and Chris Bailey-Kellogg; presented in partial fulfillment of the speaking requirement.

Web contact: sss+www@cs