The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

MSc Thesis #93110

Title:The Synthesis of Efficient Programs
Date: 1993
Abstract:The aim of this project was the synthesis of efficient (polynomial) time programs. There is a well-developed theory, Bounded Arithmetic, which synthesises all and only the polynomial time functions. The central idea behind Bounded Arithmetic is to use a restricted type of induction, PIND induction. A variant of Bounded Arithmetic was implemented in a system called MUSSEL. In this system we can automatically extract programs from proofs and evaluate the resulting programs. It is shown that all programs synthesisable in MUSSEL are polynomial time. Programs synthesised in MUSSEL are, in general, more efficient than the corresponding Oyster programs, but the proofs are, in general, longer and harder.

[Search These Pages] [DAI Home Page] [Comment]