Proving and applying program transformations expressed with second-order patterns
From MaRDI portal
Publication:1251063
Cited in
(52)- Deterministic second-order patterns
- Adapting functional programs to higher order logic
- A unification algorithm for second-order monadic terms
- A notation for lambda terms. A generalization of environments
- Unification under a mixed prefix
- A compositional framework for fault tolerance by specification transformation
- Third order matching is decidable
- Reduction and unification in lambda calculi with a general notion of subtype
- Computing in unpredictable environments: semantics, reduction strategies, and program transformations
- Program development schemata as derived rules
- An abstract formalization of correct schemas for program synthesis
- The foundation of a generic theorem prover
- Higher-order unification revisited: Complete sets of transformations
- Recursion induction principle revisited
- On the undecidability of second-order unification
- Proving theorems by reuse
- A formalized general theory of syntax with bindings: extended version
- Functions-as-constructors higher-order unification: extended pattern unification
- Mechanized metatheory revisited
- A survey of strategies in rule-based program transformation systems
- Uniform proofs as a foundation for logic programming
- Tractable and intractable second-order matching problems
- A survey of rewriting strategies in program transformation systems
- scientific article; zbMATH DE number 3896271 (Why is no real title available?)
- An axiomatic approach to the Korenjak-Hopcroft algorithms
- La fonction d'Ackermann : un nouveau mode de dérécursivation
- Infinite trees in normal form and recursive equations having a unique solution
- The variable containment problem
- 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
- A matching process modulo a theory of categorical products
- From programming-by-example to proving-by-example
- Higher-order narrowing with convergent systems
- Representing proof transformations for program optimization
- Polynomial-time inverse computation for accumulative functions with multiple data traversals
- Computing in unpredictable environments: Semantics, reduction strategies, and program transformations
- Higher-order matching for program transformation
- A Survey of the Proof-Theoretic Foundations of Logic Programming
- Equality of terms containing associative-commutative functions and commutative binding operators is isomorphism complete
- Programming by example and proving by example using higher-order unification
- More efficient bottom-up multi-pattern matching in trees
- A theory of binding structures and applications to rewriting
- The HOL-CSP Refinement Toolkit
- Types, Tableaus and Gödel’s God in Isabelle/HOL
- HOL-CSP Version 2.0
- A Sound Type System for Physical Quantities, Units, and Measurements
- Synthesis of rewrite programs by higher-order and semantic unification
- Simple second-order languages for which unification is undecidable
- Term rewriting and beyond -- theorem proving in Isabelle
This page was built for publication: Proving and applying program transformations expressed with second-order patterns
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1251063)
