Article View: comp.ai
Article #9253Seminar on program transformation at Edinburgh, 16th Oct
From: Toby Walsh
Date: Tue, 08 Oct 1991 12:45
Date: Tue, 08 Oct 1991 12:45
48 lines
3416 bytes
3416 bytes
AI Department Seminar at 2pm, 16th Oct in F10, 80 South Bridge, Edinburgh
Automated Program Transformation Through Proof Transformation
Peter Madden
Department of AI
Edinburgh University
We discuss program optimization and program adaptation (or
specialization) by the transformation of (constructive)
synthesis proofs. Synthesis proofs which yield inefficient
programs are transformed into analogous proofs which yield
more efficient programs. These proofs are based on a Martin-Lof
type theory logic and proved within the Oyster proof refinement
system.
We have implemented a system -- the meta-level
Oyster proof transformation system (MOPTS) -- for optimizing programs
through the transformation of (Oyster) synthesis proofs. The
MOPTS has the desirable properties of automatability,
correctness and various mechanisms for reducing the transformation
search space, and various control mechanisms for guiding search
through that space.
An important property of both program optimization and
program specialization, particularly regarding automation and
control, is the fact that information contained in proofs, which
may go beyond that needed for simple execution, is exploited for the
purposes of transformation: a proof will contain more information than
the program which it specifies since a program need contain no more
information than that required for execution. A proof, on the other
hand, will contain the thinking behind the program design. A main
contribution of this research stems from an investigation into how this
extra information can be exploited for the task of program
transformation.
**********************************************************
Suggestions for Dept of AI Seminar speakers are always
welcome. Please e-mail suggestions to
Toby Walsh <Toby_Walsh@ed.ac.uk>
**********************************************************
--
Toby Walsh, JANET: Toby_Walsh@uk.ac.edinburgh
Dept of Artificial Intelligence, ARPA: Toby_Walsh%uk.ac.ed@nsfnet-relay.ac.uk
80 South Bridge, UUCP: ...!ukc!ed.ac.uk!Toby_Walsh
Edinburgh EH1 1HN TEL: +44 31 650 2725
Technical Details
Message-ID:
<1991Oct8.124528.19774@aisb.ed.ac.uk>Path:
arc1-ca.pugleaf.net!gmdzi!unido!mcsun!uknet!ukc!edcastle!aisb!aisb.ed.ac.uk!twShow Full Headers
Complete Article Headers
X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 109765,ac01bec9d1e824ef,start X-Google-Attributes: gid109765,public X-Google-Thread: 160d83,ac01bec9d1e824ef,start X-Google-Attributes: gid160d83,public X-Google-Thread: 1288e1,ac01bec9d1e824ef,start X-Google-Attributes: gid1288e1,public X-Google-Thread: 1052a4,ac01bec9d1e824ef,start X-Google-Attributes: gid1052a4,public X-Google-Thread: 10461e,ac01bec9d1e824ef,start X-Google-Attributes: gid10461e,public X-Google-Thread: 11d3a4,ac01bec9d1e824ef,start X-Google-Attributes: gid11d3a4,public X-Google-ArrivalTime: 1991-10-08 12:30:59 PST Path: arc1-ca.pugleaf.net!gmdzi!unido!mcsun!uknet!ukc!edcastle!aisb!aisb.ed.ac.uk!tw From: tw@aisb.ed.ac.uk (Toby Walsh) Newsgroups: comp.ai,ai.general,ai.seminars,ai.announce,scot.announce,ed.general Subject: Seminar on program transformation at Edinburgh, 16th Oct Message-ID: <1991Oct8.124528.19774@aisb.ed.ac.uk> Date: 8 Oct 91 12:45:28 GMT Sender: news@aisb.ed.ac.uk (Network News Administrator) Reply-To: tw@aisb.ed.ac.uk (Toby Walsh) Organization: Dept AI, Edinburgh University, Scotland Lines: 48