Pages that link to "Item:Q1251063"
From MaRDI portal
The following pages link to Proving and applying program transformations expressed with second-order patterns (Q1251063):
Displaying 48 items.
- Polynomial-time inverse computation for accumulative functions with multiple data traversals (Q526439) (← links)
- More efficient bottom-up multi-pattern matching in trees (Q685356) (← links)
- A theory of binding structures and applications to rewriting (Q685380) (← links)
- Synthesis of rewrite programs by higher-order and semantic unification (Q749216) (← links)
- Simple second-order languages for which unification is undecidable (Q807609) (← links)
- Term rewriting and beyond -- theorem proving in Isabelle (Q909488) (← links)
- Deterministic second-order patterns (Q1029104) (← links)
- Adapting functional programs to higher order logic (Q1029815) (← links)
- A unification algorithm for second-order monadic terms (Q1109019) (← links)
- A notation for lambda terms. A generalization of environments (Q1129257) (← links)
- Unification under a mixed prefix (Q1201348) (← links)
- A compositional framework for fault tolerance by specification transformation (Q1330423) (← links)
- Third order matching is decidable (Q1337691) (← links)
- Reduction and unification in lambda calculi with a general notion of subtype (Q1340967) (← links)
- Computing in unpredictable environments: semantics, reduction strategies, and program transformations (Q1389440) (← links)
- Program development schemata as derived rules (Q1583853) (← links)
- An abstract formalization of correct schemas for program synthesis (Q1583858) (← links)
- The foundation of a generic theorem prover (Q1823013) (← links)
- Higher-order unification revisited: Complete sets of transformations (Q1823936) (← links)
- Recursion induction principle revisited (Q1838286) (← links)
- On the undecidability of second-order unification (Q1854349) (← links)
- Proving theorems by reuse (Q1978233) (← links)
- A formalized general theory of syntax with bindings: extended version (Q1984791) (← links)
- Functions-as-constructors higher-order unification: extended pattern unification (Q2134936) (← links)
- Mechanized metatheory revisited (Q2323447) (← links)
- A survey of strategies in rule-based program transformation systems (Q2456575) (← links)
- Uniform proofs as a foundation for logic programming (Q2640596) (← links)
- Tractable and intractable second-order matching problems (Q2643530) (← links)
- A survey of rewriting strategies in program transformation systems (Q2841225) (← links)
- Définitions récursives par cas (Q3675498) (← links)
- An axiomatic approach to the Korenjak-Hopcroft algorithms (Q3703289) (← links)
- La fonction d'Ackermann : un nouveau mode de dérécursivation (Q3737419) (← links)
- Infinite trees in normal form and recursive equations having a unique solution (Q3851585) (← links)
- The variable containment problem (Q4645807) (← links)
- Higher-order unification with dependent function types (Q5055716) (← links)
- Rewriting, and equational unification: the higher-order cases (Q5055746) (← links)
- A restricted form of higher-order rewriting applied to an HDL semantics (Q5055839) (← links)
- Higher-order superposition for dependent types (Q5055856) (← links)
- Efficient second-order matching (Q5055870) (← links)
- A matching process modulo a theory of categorical products (Q5096201) (← links)
- From programming-by-example to proving-by-example (Q5096230) (← links)
- Higher-order narrowing with convergent systems (Q5096386) (← links)
- Representing proof transformations for program optimization (Q5210798) (← links)
- Computing in unpredictable environments: Semantics, reduction strategies, and program transformations (Q5878908) (← links)
- Higher-order matching for program transformation (Q5958614) (← links)
- A Survey of the Proof-Theoretic Foundations of Logic Programming (Q6063891) (← links)
- Equality of terms containing associative-commutative functions and commutative binding operators is isomorphism complete (Q6488535) (← links)
- Programming by example and proving by example using higher-order unification (Q6488562) (← links)