Loading...
Date
2008
Abstract
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 first-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.
Supervisor
Description
non-peer-reviewed
Publisher
Citation
Ist International Workshop on Metacomputation in Russia;2008
Files
Loading...
2008_Hamilton.pdf
Adobe PDF, 210.82 KB
Keywords
ULRR Identifiers
Funding code
Funding Information
Science Foundation Ireland (SFI)
Sustainable Development Goals
External Link
Type
Meetings and Proceedings
Rights
https://creativecommons.org/licenses/by-nc-sa/1.0/