A Transformation System for Developing Recursive Programs
From MaRDI portal
Publication:4111080
DOI10.1145/321992.321996zbMath0343.68014OpenAlexW2023299380MaRDI QIDQ4111080
John Darlington, Rod M. Burstall
Publication date: 1977
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.19.4684
Related Items
Evolution of rule-based programs ⋮ A parallel algorithm for the monadic unification problem ⋮ NTS languages are deterministic and congruential ⋮ On the creation of a macromodel of social development ⋮ Denotational semantics of a para-functional programming language ⋮ Partial parametrization eliminates multiple traversals of data structures ⋮ Counterexample-guided partial bounding for recursive function synthesis ⋮ Rules + strategies for transforming lazy functional logic programs ⋮ Algebraic specification and proof of a distributed recovery algorithm ⋮ Derivation of efficient programs for computing sequences of actions ⋮ A transformation method for dynamic-sized tabulation ⋮ Asymptotic Speedups, Bisimulation and Distillation (Work in Progress) ⋮ A relation algebraic model of robust correctness ⋮ Equivalences and transformations of regular systems - applications to recursive program schemes and grammars ⋮ A recursion planning analysis of inductive completion ⋮ Mechanical translation of set theoretic problem specifications into efficient RAM code - a case study ⋮ Abstract language design ⋮ Formalized program specifications and transformation synthesis ⋮ On fuzzy unfolding: A multi-adjoint approach ⋮ Composing recursive logic programs with clausal join ⋮ Things to know when implementing KBO ⋮ A calculus of refinements for program derivations ⋮ Existential continuation ⋮ The McCarthy's recursion induction principle: oldy but goody ⋮ On the transformation of logic programs with instantiation based computation rules ⋮ Lambda calculus with explicit recursion ⋮ Optimization of rewrite theories by equational partial evaluation ⋮ Schema induction for logic program synthesis ⋮ Deaccumulation techniques for improving provability ⋮ Final algebra semantics and data type extensions ⋮ Horn Clause Solvers for Program Verification ⋮ Determinization of conditional term rewriting systems ⋮ Computing in unpredictable environments: semantics, reduction strategies, and program transformations ⋮ A logical semantics for depth-first Prolog with ground negation ⋮ Partially additive categories and flow-diagram semantics ⋮ Prolegomena to a theory of mechanized formal reasoning ⋮ Towards ``mouldable code via nested code graph transformation ⋮ Object grammars and bijections. ⋮ Constraint-based correctness proofs for logic program transformations ⋮ An algebraic definition for control structures ⋮ A strange sorting method inspired by formal differentiation ⋮ First order compiler: A deterministic logic program synthesis algorithm ⋮ Term rewriting and beyond -- theorem proving in Isabelle ⋮ Automated verification of shape, size and bag properties via user-defined predicates in separation logic ⋮ On correct refinement of programs ⋮ An efficient interpreter for the lambda-calculus ⋮ A reification calculus for model-oriented software specification ⋮ Deforestation: Transforming programs to eliminate trees ⋮ Preservation of stronger equivalence in unfold/fold logic program transformation ⋮ Hume box calculus: Robust system development through software transformation ⋮ Algebraic fusion of functions with an accumulating parameter and its improvement ⋮ A survey of strategies in rule-based program transformation systems ⋮ Derivation of logic programs by functional methods ⋮ A new approach to recursion removal ⋮ Transformations of CLP modules ⋮ Proving the correctness of recursion-based automatic program transformations ⋮ Loop detection in term rewriting using the eliminating unfoldings ⋮ Unfolding--definition--folding, in this order, for avoiding unnecessary variables in logic programs ⋮ The functional dimension of inductive definitions ⋮ Optimizing the stack size of recursive functions ⋮ Rippling: A heuristic for guiding inductive proofs ⋮ Short note: Strict unwraps make worker/wrapper fusion totally correct ⋮ Equivalence-preserving first-order unfold/fold transformation systems ⋮ Unfolding and fixpoint semantics of concurrent constraint logic programs ⋮ Algebraic optimization of object-oriented query languages ⋮ Program morphisms ⋮ Transformations of logic programs on infinite lists ⋮ Fixpoints for general correctness ⋮ Totally correct logic program transformations via well-founded annotations ⋮ Efficient memo-table management strategies ⋮ The worker/wrapper transformation ⋮ Provably correct derivation of algorithms using FermaT ⋮ A partial evaluation framework for order-sorted equational programs modulo axioms ⋮ Program transformations and algebraic semantics ⋮ Analogical program derivation based on type theory ⋮ Inferring expected runtimes of probabilistic integer programs using expected sizes ⋮ Semantics of algorithmic languages ⋮ Transforming constraint logic programs ⋮ Synthetic programming ⋮ Logic program forms ⋮ Extraction and verification of programs by analysis of formal proofs ⋮ An improved reductant calculus using fuzzy partial evaluation techniques ⋮ Recursion induction principle revisited ⋮ Derivation of an \(O(k^ 2\log n)\) algorithm for computing order-k Fibonacci numbers from the \(O(k^ 3\log n)\) matrix multiplication method ⋮ Some equivalent transformations of recursive programs based on their schematic properties ⋮ On synthesis of scheduling algorithms ⋮ Automatic programming: A tutorial on formal methodologies ⋮ Using circular programs to eliminate multiple traversals of data ⋮ Propositions and specifications of programs in Martin-Löf's type theory ⋮ Top-down synthesis of divide-and-conquer algorithms ⋮ Mixtus: An automatic partial evaluator for full Prolog ⋮ Efficient Reductants Calculi using Partial Evaluation Techniques with Thresholding ⋮ Logic program synthesis from first-order logic specifications ⋮ Towers of Hanoi problems: deriving iterative solutions by program transformations ⋮ Compiling bottom-up and mixed derivations into top-down executable logic programs ⋮ Experiments with proof plans for induction ⋮ Work it, wrap it, fix it, fold it ⋮ Deductive and inductive synthesis of equational programs ⋮ Deriving fold/unfold transformations of logic programs using extended OLDT-based abstract interpretation ⋮ Derivation of efficient logic programs by specialization and reduction of nondeterminism ⋮ Fold–unfold lemmas for reasoning about recursive programs using the Coq proof assistant ⋮ Rewriting techniques for program synthesis ⋮ Program transformation and rewriting ⋮ Automatically Introducing Tail Recursion in CakeML ⋮ Abstracting Models from Execution Traces for Performing Formal Verification ⋮ LOGIC DERIVATION OF PARALLEL LINEAR EQUATION SYSTEM SOLVERS WITHIN ELIMINATION STRATEGY ⋮ Unnamed Item ⋮ La fonction d'Ackermann : un nouveau mode de dérécursivation ⋮ Unfold/fold transformations of logic programs ⋮ Unnamed Item ⋮ An equivalence preserving first order unfold/fold transformation system ⋮ Symbolic Specialization of Rewriting Logic Theories with Presto ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ Folding left and right matters: Direct style, accumulators, and continuations ⋮ The next 700 program transformers ⋮ Excommunication: transforming \(\pi \)-calculus specifications to remove internal communication ⋮ Applying Constraint Logic Programming to SQL Semantic Analysis ⋮ Optimizing Maude programs via program specialization ⋮ A positive supercompiler ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Inverse Unfold Problem and Its Heuristic Solving ⋮ Program derivation with verified transformations — a case study ⋮ Unnamed Item ⋮ Formal basis for the refinement of rule based transition systems ⋮ Manipulating accumulative functions by swapping call-time and return-time computations ⋮ Logical approach to control theory and applications ⋮ Fold/Unfold Transformations for Fixpoint Logic ⋮ Deforestation, program transformation, and cut-elimination ⋮ A Case Study in Abstract Interpretation Based Program Transformation ⋮ Optimizing Fuzzy Logic Programs by Unfolding, Aggregation and Folding ⋮ A higher-order interpretation of deductive tableau ⋮ Infinite trees in normal form and recursive equations having a unique solution ⋮ Using transformations in the implementation of higher-order functions ⋮ The narrowing-driven approach to functional logic program specialization ⋮ Program transformation system based on generalized partial computation ⋮ Representing proof transformations for program optimization ⋮ Proving the correctness of recursion-based automatic program transformations ⋮ Efficient Unfolding of Fuzzy Connectives for Multi-adjoint Logic Programs ⋮ Symbolic Unfolding of Multi-adjoint Logic Programs ⋮ Folding left and right over Peano numbers ⋮ Unfolding and fixpoint semantics of concurrent constraint logic programs ⋮ “Curiouser and curiouser” said alice. further reflections on an interesting recursive function ⋮ A Folding Algorithm for Eliminating Existential Variables from Constraint Logic Programs ⋮ How powerful are folding/unfolding transformations? ⋮ Lilac: a functional programming language based on linear logic ⋮ Total unfolding: theory and applications ⋮ Computing in unpredictable environments: Semantics, reduction strategies, and program transformations
