Home News About Us Contact Contributors Disclaimer Privacy Policy Help FAQ

Home
Search
Quick Search
Advanced
Fulltext
Browse
Collections
Persons
My eDoc
Session History
Login
Name:
Password:
Documentation
Help
Support Wiki
Direct access to
document ID:


          Institute: MPI für Informatik     Collection: Programming Logics Group     Display Documents



ID: 519767.0, MPI für Informatik / Programming Logics Group
Program Development Schemata as Derived Rules
Authors:Anderson, Penny; Basin, David A.
Language:English
Date of Publication (YYYY-MM-DD):2000
Title of Journal:Journal of Symbolic Computation
Volume:30
Issue / Number:1
Start Page:5
End Page:36
Review Status:Peer-review
Audience:Experts Only
Intended Educational Use:No
Abstract / Description:We show how the formalization and application of schemata for program
development can be reduced to the formalization and application of
derived rules of inference. We formalize and derive schemata as rules
in theories that axiomatize program data and programs themselves. We
reduce schema-based program development to ordinary theorem proving,
where higher-order unification is used to apply rules. Conceptually,
our formalization is simple and unifies divergent views of schemata,
program synthesis, and program transformation.
Practically, our formalization yields a simple methodology for
carrying out development using existing logical frameworks; we
illustrate this in the domain of logic program synthesis and
transformation using the Isabelle logical framework.
Last Change of the Resource (YYYY-MM-DD):2010-03-12
External Publication Status:published
Document Type:Article
Communicated by:Andreas Podelski
Affiliations:MPI für Informatik/Programming Logics Group
Identifiers:LOCALID:C1256104005ECAFC-7753DE65EF5CDC83C12568B20045C96E-...
ISSN:0747-7171
The scope and number of records on eDoc is subject to the collection policies defined by each institute - see "info" button in the collection browse view.