A computer program is written in a high-level *programming* *language*, but to be run, it must be translated into a *machine* *language*. Each kind of machine---desktop computer, cell phone, handheld computer---has a different machine language and needs a different translator. At present, each translator must be written by an expert who specializes *both* in translation *and* in machine language. This project will develop methods by which a translator can be written without such double expertise. An expert who knows only about the machine will write a *declarative* description that says what the machine does. The project's software will analyze this description and mechanically produce components to be used by an expert who knows only about translation. Because this approach relies crucially on the description's being correct, the project will also develop techniques for mechanically checking that the description is consistent with real hardware. The descriptions and the analysis thereof will enable the machine expert's work to be reused in many different translators (and other applications) and the translation expert's work to be readily applied to many different machines. Translators for new machines will be developed more quickly, more reliably, and with less effort than at present.
