
SSS Abstracts Fall 2008 

RealTime GradientDomain Painting
Friday, September 19^{th}, 2008 from 121 pm in Wean 5409.
In my gradientdomain 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 (GPUbased multigrid) that keeps things running at interactive rates, and the brushes and blend modes that allow users to perform gradientdomain edits.
If you'd like to try out the paint system (and have a decent graphics card), visit http://gradientpaint.com where you can find binaries for Linux, OSX, and Windows as well as source code.
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
"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", "patternmatching", 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 (patternmatching). 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 CurryHoward 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.)
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 programminge.g., implementing compilers and theorem proversand for provinge.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.
The behavior of a biomolecular 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 BaileyKellogg; presented in partial fulfillment of the speaking requirement.
Web contact: sss+www@cs