9801581 Jaffe This award supports research on a project involving the search for and implementation of alogorithms for classifying optimal linear codes, with an emphasis on the binary case. Included here is the problem of discovering new optimal linear codes and describing them in a meaningful way. All of this is part of the ongoing development of a computer language Split, which facilitates the mechanical verification of proofs about linear codes. This research concerns optimal error-correcting codes, which play a ubiquitous role in modern technology, because they make possible the transmission of information across noisy channels. For example, such codes facilitate earth-satellite communications (in spite of atmospheric disturbances), and such codes facilitate the reading of compact disks (in spite of dust and damage to the disk's surface). Codes are abstract mathematical objects. Those that are are most effective for transmitting information are called optimal. It is an open mathematical problem - and the subject of this research - to determine just how effective a code can be. This problem can be converted into a computational problem called "linear programming", which is also used by many industries (such as the airline industry) to optimize their use of resources. As existing linear programming software is not good enough to answer the problems arising from coding theory, new software will be developed. In addition, software which allows for the mechanical verification of assertions about codes will provide a "front end" to these linear programming calculations. All such software (including source code) will be made freely available to the public.