Combinatory reduction systems: Introduction and survey
From MaRDI portal
This paper investigates combinatory reduction systems (CRSs), i.e. usual first-order term rewriting systems with the presence of bound variables. It introduces orthogonal CRSs (illustrated with many examples) and gives an outline of the proof of confluence. It also shows an extension of the finite development theorem.
Recommendations
Cites work
- A complete inference system for a class of regular behaviours
- A theory of binding structures and applications to rewriting
- Combinators, \(\lambda\)-terms and proof theory
- Confluence and superdevelopments
- Confluence of the lambda calculus with left-linear algebraic rewriting
- scientific article; zbMATH DE number 3646849 (Why is no real title available?)
- scientific article; zbMATH DE number 3122413 (Why is no real title available?)
- scientific article; zbMATH DE number 4158597 (Why is no real title available?)
- scientific article; zbMATH DE number 4033738 (Why is no real title available?)
- scientific article; zbMATH DE number 4048997 (Why is no real title available?)
- scientific article; zbMATH DE number 3684935 (Why is no real title available?)
- scientific article; zbMATH DE number 3707731 (Why is no real title available?)
- scientific article; zbMATH DE number 3730111 (Why is no real title available?)
- scientific article; zbMATH DE number 3735770 (Why is no real title available?)
- scientific article; zbMATH DE number 51605 (Why is no real title available?)
- scientific article; zbMATH DE number 108365 (Why is no real title available?)
- scientific article; zbMATH DE number 3523519 (Why is no real title available?)
- scientific article; zbMATH DE number 4124996 (Why is no real title available?)
- scientific article; zbMATH DE number 512788 (Why is no real title available?)
- scientific article; zbMATH DE number 512795 (Why is no real title available?)
- scientific article; zbMATH DE number 515729 (Why is no real title available?)
- scientific article; zbMATH DE number 1142316 (Why is no real title available?)
- scientific article; zbMATH DE number 1142317 (Why is no real title available?)
- scientific article; zbMATH DE number 194511 (Why is no real title available?)
- scientific article; zbMATH DE number 3993540 (Why is no real title available?)
- scientific article; zbMATH DE number 3999882 (Why is no real title available?)
- scientific article; zbMATH DE number 3358455 (Why is no real title available?)
- LCF considered as a programming language
- Modular properties of conditional term rewriting systems
- On the longest perpetual reductions in orthogonal expression reduction systems
- Pairing Without Conventional Restraints
- Parallel reductions in \(\lambda\)-calculus
- Rewriting, and equational unification: the higher-order cases
- Sequential evaluation strategies for parallel-or and related reduction systems
- Standard and Normal Reductions
- The Clausal Theory of Types
- The Equivalence of Complete Reductions
- The lambda calculus. Its syntax and semantics. Rev. ed.
- Unique normal forms for lambda calculus with surjective pairing
Cited in
(80)- Higher-order rewrite systems and their confluence
- Order-sorted inductive types
- Combining algebraic rewriting, extensional lambda calculi, and fixpoints
- Interaction systems II: The practice of optimal reductions
- Strong normalization from weak normalization in typed \(\lambda\)-calculi
- Lambda calculus with explicit recursion
- Computing in unpredictable environments: semantics, reduction strategies, and program transformations
- Developing developments
- Theorem proving modulo
- Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions
- Checking overlaps of nominal rewriting rules
- Normalisation for higher-order calculi with explicit substitutions
- Descendants and origins in term rewriting.
- Perpetuality and uniform normalization in orthogonal rewrite systems
- Normal forms in combinatory logic
- Counterexamples in infinitary rewriting with non-fully-extended rules
- Logical foundations for hybrid type-logical grammars
- Nominal rewriting
- On explicit substitution with names
- Expression reduction systems with patterns
- Higher-order interpretations and program complexity
- Nominal confluence tool
- Introducing a calculus of effects and handlers for natural language semantics
- Rewriting calculus with(out) types
- A framework for defining logical frameworks
- From functional programs to interaction nets via the rewriting calculus
- The power of closed reduction strategies
- Complete laziness: a natural semantics
- Token-passing nets for functional languages
- Three Syntactic Theories for Combinatory Graph Reduction
- The algebra of recursive graph transformation language UnCAL: complete axiomatisation and iteration categorical semantics
- Harnessing first order termination provers using higher order dependency pairs
- Converting between Combinatory Reduction Systems and Big Step Semantics
- scientific article; zbMATH DE number 4208054 (Why is no real title available?)
- Strong normalisation in two Pure Pattern Type Systems
- On Normalisation of Infinitary Combinatory Reduction Systems
- Comparing Böhm-Like Trees
- On the Relation between Sized-Types Based Termination and Semantic Labelling
- scientific article; zbMATH DE number 32501 (Why is no real title available?)
- scientific article; zbMATH DE number 1303339 (Why is no real title available?)
- Labelled reductions, runtime errors, and operational subsumption
- Size-based termination of higher-order rewriting
- A metamodel of access control for distributed environments: applications and properties
- The variable containment problem
- Abstract reduction systems and idea of Knuth-Bendix completion algorithm
- Axiomatizing permutation equivalence
- Confluence and superdevelopments
- Combinatory reduction systems with explicit substitution that preserve strong normalisation
- Dependency pairs termination in dependent type theory modulo rewriting
- Recursive Functions with Pattern Matching in Interaction Nets
- scientific article; zbMATH DE number 5201482 (Why is no real title available?)
- Infinitary combinatory reduction systems
- Term Rewriting and Applications
- Interaction nets and term rewriting systems (extended abstract)
- A modular construction of type theories
- Processes, Terms and Cycles: Steps on the Road to Infinity
- A new connective in natural deduction, and its application to quantum computing
- Variable binding operators in transition system specifications
- Inductive-data-type systems
- On the longest perpetual reductions in orthogonal expression reduction systems
- A prismoid framework for languages with resources
- Minimal relative normalization in orthogonal expression reduction systems
- On basic feasible functionals and the interpretation method
- Sharing proofs with predicative theories through universe-polymorphic elaboration
- Intersection type assignment systems with higher-order algebraic rewriting
- Wanda -- a higher-order termination tool (system description)
- The new rewriting engine of dedukti (system description)
- Type safety of rewrite rules in dependent types
- Realizability at work: separating two constructive notions of finiteness
- A characterization of basic feasible functionals through higher-order rewriting and tuple interpretations
- Sort-based confluence criteria for non-left-linear higher-order rewriting
- Closed nominal rewriting and efficiently computable nominal algebra equality
- Encoding of predicate subtyping with proof irrelevance in the -calculus modulo theory
- Introducing \(\llparenthesis\lambda\rrparenthesis\), a \(\lambda \)-calculus for effectful computation
- Expressing combinatory reduction systems derivations in the rewriting calculus
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
- Capture-avoiding substitution as a nominal algebra
- Gödel's system T revisited
- Matching and alpha-equivalence check for nominal terms
- On the confluence of lambda-calculus with conditional rewriting
This page was built for publication: Combinatory reduction systems: Introduction and survey
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1314356)
