Proving and applying program transformations expressed with second-order patterns
From MaRDI portal
Publication:1251063
DOI10.1007/BF00264598zbMath0389.68008OpenAlexW2062968803WikidataQ56608660 ScholiaQ56608660MaRDI QIDQ1251063
Publication date: 1978
Published in: Acta Informatica (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/bf00264598
Related Items
A compositional framework for fault tolerance by specification transformation, An axiomatic approach to the Korenjak-Hopcroft algorithms, Third order matching is decidable, Functions-as-constructors higher-order unification: extended pattern unification, Reduction and unification in lambda calculi with a general notion of subtype, Higher-order unification with dependent function types, Rewriting, and equational unification: the higher-order cases, A restricted form of higher-order rewriting applied to an HDL semantics, Higher-order superposition for dependent types, Efficient second-order matching, Uniform proofs as a foundation for logic programming, Tractable and intractable second-order matching problems, A unification algorithm for second-order monadic terms, La fonction d'Ackermann : un nouveau mode de dérécursivation, A notation for lambda terms. A generalization of environments, A matching process modulo a theory of categorical products, From programming-by-example to proving-by-example, Higher-order narrowing with convergent systems, Computing in unpredictable environments: semantics, reduction strategies, and program transformations, A Survey of the Proof-Theoretic Foundations of Logic Programming, Term rewriting and beyond -- theorem proving in Isabelle, A survey of strategies in rule-based program transformation systems, Proving theorems by reuse, A formalized general theory of syntax with bindings: extended version, The variable containment problem, Unnamed Item, More efficient bottom-up multi-pattern matching in trees, A theory of binding structures and applications to rewriting, Unification under a mixed prefix, Polynomial-time inverse computation for accumulative functions with multiple data traversals, Infinite trees in normal form and recursive equations having a unique solution, Higher-order matching for program transformation, Representing proof transformations for program optimization, Synthesis of rewrite programs by higher-order and semantic unification, Deterministic second-order patterns, Adapting functional programs to higher order logic, The foundation of a generic theorem prover, Higher-order unification revisited: Complete sets of transformations, Mechanized metatheory revisited, A Survey of Rewriting Strategies in Program Transformation Systems, Recursion induction principle revisited, Program development schemata as derived rules, An abstract formalization of correct schemas for program synthesis, On the undecidability of second-order unification, Simple second-order languages for which unification is undecidable, Computing in unpredictable environments: Semantics, reduction strategies, and program transformations
Uses Software
