μετα 2008

First International Workshop on Metacomputation in Russia
 

July 2-5, 2008, Pereslavl-Zalessky (120 km to the north-east from Moscow), Russia

Home
Call For Papers
Submissions
Accepted Papers
Program
Important Dates
Registration
Visa Support
Place
Affiliated Meetings
Contacts
Sponsors

 

 

 

 

Constructing Programs From Metasystem Transition Proofs

G.W. Hamilton and M.H. Kabir
 

Abstract

Full text pdf 259 KB

It has previously been shown by Turchin in the context of supercompilation how metasystem transitions can be used in the proof of universally and existentially quantified conjectures. Positive supercompilation is a variant of Turchin's supercompilation which was introduced in an attempt to study and explain the essentials of Turchin's supercompiler. In our own previous work, we have proposed a program transformation algorithm called distillation, which is more powerful than positive supercompilation, and have shown how this can be used to prove a wider range of universally and existentially quantified conjectures in our theorem prover Poitín. In this paper we show how a wide range of programs can be constructed fully automatically from rst-order specifications through the use of metasystem transitions, and we prove that the constructed programs are totally correct with respect to their specifications. To our knowledge, this is the first technique which has been developed for the automatic construction of programs from their specifications using metasystem transitions.