1. Background

Frequently, working software developers will encounter a problem with which they are unfamiliar, but which - they suspect - has probably been treated by the Computer Science theory community. Just as frequently, theoretical computer scientists will be working on a problem which they suspect might have a practical application.

Unfortunately, the programmer with a problem in search of a solution and the theoretician with a solution in search of an application are unlikely to connect across the geographical and linguistic chasm that often separate the two. In many organizations working programmers do not have easy access to a theoretician, and, when they do, they often find communication difficult.

In this paper we will describe A$\lambda$goVista, a web-based, interactive, searchable, and extensible database of problems and algorithms designed to bring together applied and theoretical computer scientists. Working programmers can query A$\lambda$goVista to look for theoretical results that are relevant to their current application. Theoretical computer scientists can extend A$\lambda$goVista with problems with which they are familiar, or with references to new algorithms they have developed for these problems.

A$\lambda$goVista is based on a novel application of a technique known as program (or result) checking, developed over the last decade by Manuel Blum and others [10,4,5,19,6,16,17] as an alternative to program verification and testing. Program checking extends programs with checkers to allow them to verify the correctness of the results they compute.