Alessandro Armando, Alan Smaill, Ian Green  @ NUS Home/Search
Context Related
| ase.informatik.uniess...97Smaill.ps.gz Cached: PS.gz PS PDF Image Update Help From: ase.informatik.uniessen.de/ol... (more) (Enter author homepages) |
Rate this article:      (best)Comment on this article |
Abstract: We describe a proof plan that characterises a family of proofs corresponding to the synthesis of recursive functional programs. This plan provides a significant degree of automation in the construction of recursive programs from specifications, together with correctness proofs. This plan makes use of meta-variables to allow successive refinement of the identity of unknowns, and so allows the program and the proof to be developed hand in hand. We illustrate the plan with parts of a substantial... (Update)
Context of citations to this paper: More
...from non existential ones. This, however, increases the search problem in the presence of existential quantifiers. Other approaches [1, 17, 25] use meta annotations, which requires higher order unification and may lead to non terminating rippling sequences. The approach...
...order logic in the Clam proof planning engine instead of the rst order logic of the Clam proof planner. Smaill, Green [SG95] and Armando [ASG97] used Clam as the basis for the synthesis of functional programs. Induction using the rippling heuristic is used to guide the...
Cited by: More
Combining Proof Plans with Partial Order Planning for - Imperative Program Synthesis (Correct)
A Unified View of Program Schemas and Proof Methods - Flener, Richardson (Correct)
Higher Order Function Synthesis Through Proof Planning - Andrew Cook Andrew (2001) (Correct)
Similar documents (at the sentence level):
76.8%: Automatic Synthesis of Recursive Programs: The.. - Armando, Smaill, Green (1997) (Correct)
7.7%: Automating the Synthesis of Functional Programs - Smaill, Green (1995) (Correct)
Active bibliography (related documents): More All
0.3: Fundamentals Of Deductive Program Synthesis - Manna, Waldinger (1992) (Correct)
0.3: Automating the Synthesis of Decision Procedures - Armando, Gallagher, Smaill (1994) (Correct)
0.3: Unification - Nardi (Correct)
Similar documents based on text: More All
0.4: MRG: Building Planners for Real World Complex Applications - Traverso, Cimatti.. (1994) (Correct)
0.4: First Steps Towards Correct System Synthesis of System.. - Giunchiglia, Armando.. (1994) (Correct)
0.3: Navigation By Combining Reactivity and Planning - Cimatti, Traverso, Dalbosco.. (1992) (Correct)
Related documents from co-citation: More All
9: Rippling:a heuristic for guiding inductive proofs - Bundy, Stevens et al. - 1993
7: A calculus for and termination of rippling - Basin, Walsh - 1996
6: Logic program synthesis via proof planning - Kraan, Basin et al. - 1993
BibTeX entry: (Update)
A. Armando, A. Smaill, and I. Green. Automatic synthesis of recursive programs: The proof-planning paradigm. In 12 th IEEE International Automated Software Engineering Conference, pp. 2--9. IEEE Computer Society, 1997. http://citeseer.comp.nus.edu.sg/666039.html More
@misc{ armando97automatic,
author = "A. Armando and A. Smaill and I. Green",
title = "Automatic synthesis of recursive programs: The proof-planning paradigm",
text = "A. Armando, A. Smaill, and I. Green. Automatic synthesis of recursive programs:
The proof-planning paradigm. In 12 th IEEE International Automated Software
Engineering Conference, pp. 2--9. IEEE Computer Society, 1997.",
year = "1997",
url = "citeseer.comp.nus.edu.sg/666039.html" }
Citations (may not include all citations):505 Implementing Mathematics with the Nuprl Proof Development Sy.. - Constable, Allen et al. - 1986
275 The Science of Programming (context) - Gries - 1981
233 The formulae-as-types notion of construction (context) - Howard - 1980
226 The use of explicit plans to guide inductive proofs - Bundy - 1988
168 Rippling: A heuristic for guiding inductive proofs - Bundy, Stevens et al. - 1993
163 Application of theorem proving to problem solving (context) - Green
94 A deductive approach to program synthesis (context) - Manna, Waldinger - 1980
61 Deductive composition of astronomical software from subrouti.. - Stickel, Waldinger et al. - 1994
28 Logic program synthesis via proof planning - Kraan, Basin et al. - 1993
27 Deductive synthesis of the unification algorithm (context) - Manna, Waldinger - 1981
24 A rational reconstruction and extension of recursion analysi.. - Bundy, van Harmelen et al. - 1989
21 Verifying the unification algorithm in lcf - Paulson - 1984
19 Implementing metamathematics as an approach to automatic the.. (context) - Constable, Howe - 1990
17 Synthesis and transformation of logic programs in the Whelk .. (context) - Wiggins - 1992
16 Programming in Martin-Lof Type Theory (context) - Nordstrom, Petersson et al. - 1990
13 Automated synthesis of recursive algorithms as a theorem pro.. (context) - Biundo - 1988
12 Annotated rewriting in inductive theorem proving (context) - Basin, Walsh - 1996
12 PROW: A step toward automatic program writing (context) - Waldinger, Lee
12 Logic frameworks for logic programs - Basin - 1994
11 A natural programming calculus (context) - Hanson, S- - 1979
9 s programs from proofs in the calculus of constructions (context) - Paulin-Mohring - 1989
9 Abstractions in logic programs (context) - Miller - 1990
5 Proof planning: a methodology for developing AI systems invo.. (context) - Lowe - 1994
4 The Use of Proof Plans in Tactic Synthesis (context) - Gallagher - 1993
4 Synthesis of a unification algorithm in a logic programming .. (context) - Eriksson - 1984
3 Formal synthesis of a unification algorithm by the deductive.. (context) - Nardi - 1989
The graph only includes citing articles where the year of publication is known.
Documents on the same site (http://ase.informatik.uni-essen.de/olbib/): More
Exploring and Validating the Contributions of Real-World.. - Noah, Williams (Correct)
Renaming Detection - Malpohl, Hunt, Tichy (2000) (Correct)
Interactive Explanation of Software Systems - Johnson, Erdem (1996) (Correct)
Online articles have much greater impact More about CiteSeer.IST at NUS Add search form to your site Submit documents Feedback
CiteSeer.IST at NUS - Copyright Penn State and NEC. Hosted by the School of Computing, National University of Singapore.