go back to the main page

 SSS Abstracts 
Spring 2001

go back to the main page

Reasoning about resources with linear logic.

Friday, March 30th, 2001 from 12-1 pm in NSH 1507.

Presented by Jeffrey Polakow,

The need to reason about resources often arises in computer science. Examples may be found in such disparate domains as planning problems in AI or garbage collection in programming languages. However, using intuitionistic (or classical) logic to reason about resources often requires awkward logical machinery to accurately model resource consumption. In this talk I will present a relatively new logic, linear logic, and show how it allows for very natural encodings of, and reasoning about, resources.

Knowledge of Language Origin Improves Pronunciation Accuracy of Proper Names

Friday, April 13th, 2001 from 12-1 pm in NSH 1507.

Presented by Ariadna Font Llitjos,

In the same way that we seem to adapt our pronunciation according to where we think a foreign proper names comes from, my experiments show that adding language probabilities to the pronunciation model (CART) actually improves pronunciation word accuracy by 7.6% (from a proper name baseline). To get these features, I built a language identifier for 26 languages, including Japanese, Chinese, Korean and Thai. User studies have shown that the perceived accuracy is 60% higher for the model that uses language probabilities than for the baseline.

NanoFabrics: Spatial Computing using Molecular Electronics

Friday, April 20th, 2001 from 12-1 pm in NSH 1507.

Presented by Mihai Budiu,

The continuation of the remarkable exponential increases in processing power over the recent past faces imminent challenges due in part to the physics of deep-submicron CMOS devices and the costs of both chip masks and future fabrication plants. A promising solution to these problems is offered by an alternative to CMOS-based computing, chemically assembled electronic nanotechnology (CAEN).

In this talk I will outline how CAEN-based computing can become a reality. I will briefly describe recent work in CAEN and how CAEN will affect computer architecture. I will show how the inherently reconfigurable nature of CAEN devices can be exploited to provide high-density chips with defect tolerance at significantly reduced manufacturing costs. I will also present preliminary results which indicate that such devices will be competitive with CMOS circuits.

Joint work with Seth Copen Goldstein and Dan Rosewater.

This talk is in partial fulfillment of the speaking requirement.

Automatic Generation of Staged Geometric Predicates

Friday, April 27th, 2001 from 12-1 pm in NSH 1507.

Presented by Aleksandar Nanevski,

Algorithms in Computational Geometry are often developed for the Real RAM model of computation, which assumes exactness of all the input arguments and operations. In practice, however, the exactness imposes tremendous limitations on the algorithms -- even the basic operations become uncomputable, or prohibitively slow. When the computations of interest are limited to determining the sign of polynomial expressions over floating point numbers, faster approaches are available. One can evaluate the polynomial in floating point first, together with some estimate of the rounding error, and fall back to exact arithmetic only if this error is too big to determine the sign reliably. We present a method for automatic generation of this kind of floating point predicates from their exact mathematical counterparts.

This is joint work with Guy Blelloch and Robert Harper.

Shadow of the Lizard: Open Problems Inspired By The Mozilla Project

Friday, May 4th, 2001 from 12-1 pm in NSH 1507.

Presented by Robert O'Callahan,

Mozilla is the open-source Web browser project run by Netscape/AOL. In this talk I will survey a few of its challenging technical problems with a researcher's eye, and attempt to persuade the audience that they represent interesting, largely unexplored territory for future research.

Code Interoperation: Modern systems like Mozilla must support tight integration of code written in multiple languages such as C, C++, Java and Javascript. Microsoft's .NET tries to map everything onto a single bytecode instruction set and runtime system, but many language features and implementation strategies don't fit into the framework. Can we design a system which gives maximal freedom to language designers and implementors while achieving interoperability goals in areas such as control flow, types, garbage collection and concurrency?

Cooperative Resource Management: Mozilla contains a large number of caches, not just to hide I/O latency but also to avoid expensive recomputations (e.g., decompressed image data is cached). How should memory be allocated to the caches to maximise system performance?

Feature Factoring: Web documents make use of a plethora of overlapping features various markup languages, various style languages with associated presentation requirements, and various "ilities" such as incrementality. How can the implementation of these features in a Web browser be modularized in a rational, future-proof way?

Verifying the Termination of Programs

Friday, May 11th, 2001 from 12-1 pm in NSH 1507.

Presented by Brigitte Pientka,

The benefits of type-checking in current programming languages have been widely recognized in recent years. However, type-checking only guarantees a very weak form of consistency: we can write many programs which are well-typed, but their evaluation leads to an infinite loop. Although completely automatic methods for proving termination are being developed in the area of software verification, they are neither feasible nor desirable in the practice of programming. I discuss why and explain an unobtrusive mechanism which allows the programmer to provide key information needed to facilitate verifying program termination. The proposed method assists the programmer with detecting errors, such as infinite loops, leading to more robust programs.

This talk is in partial fulfillment of the speaking requirement.

BoB: An Improvisational Music Companion

Friday, May 18th, 2001 from 12-1 pm in NSH 1507.

Presented by Belinda Thom,

In this talk, I will describe a new melody representation scheme and a machine learning framework that enables customized interaction between a live, improvising musician and the computer. The ultimate intent of these technologies is to provide the infrastructure needed to intimately couple the computer with a musician's all-too-transient improvisations. Potential applications include improvisational exploration, education, and musical analysis. As an instantiation of these technologies, I will introduce Band-OUT-of-a-Box (BoB), an agent that trades personalized solos with its user. Musical improvisation is an ill-defined situation- and user-specific practice whose inherent non-literal basis means that the authoring techniques often exploited in other AI-and-entertainment-based systems (e.g., interactive characters, stories, and worlds) are less applicable here. BoB addresses this issue by introducing a computational model of melodic improvisation that configures itself with respect to users' unlabeled examples.

In detailing the system, I will first describe an abstract perception algorithm that maps short strings of notes onto a mixture model. The components of this model correspond to the various "playing modes" (tonal, intervallic, and directional trends) that the user has employed during various parts of his or her improvisation. Next, I will present an abstract generation algorithm that seamlessly integrates a particular "playing mode" with a probabilistic graph to produce novel note sequences in that mode. The generation algorithm addresses difficulties in combining different levels of temporal abstraction to form a viable note sequence; for example, how does one arrange a desired set of pitches so as to produce the desired set of intervals? Finally, I will aesthetically evaluate my algorithms' performance by analyzing and contrasting two different versions of BoB: one trained on the transcriptions of Bebop saxophonist Charlie Parker and the other on jazz violinist Stephane Grappelli. The quantitative performance of these algorithms will also be assessed using traditional machine learning techniques.

Web contact: sss+www@cs