Combinatory reduction systems: Introduction and survey

DOI10.1016/0304-3975(93)90091-7zbMATH Open0796.03024OpenAlexW4212868911MaRDI QIDQ1314356FDOQ1314356

Vincent van Oostrom, Femke van Raamsdonk, Jan Willem Klop

Publication date: 26 September 1994

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://ir.cwi.nl/pub/5233

zbMATH Keywords

confluencelambda calculusterm rewriting systemscombinatory reduction systemsextension of the finite developments theorem

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)

Cites Work

• LCF considered as a programming language
• The lambda calculus. Its syntax and semantics. Rev. ed.
• A complete inference system for a class of regular behaviours
• Modular properties of conditional term rewriting systems
• The Clausal Theory of Types
• Sequential evaluation strategies for parallel-or and related reduction systems
• Parallel reductions in \(\lambda\)-calculus
• A theory of binding structures and applications to rewriting
• Unique normal forms for lambda calculus with surjective pairing
• Pairing Without Conventional Restraints
• Combinators, \(\lambda\)-terms and proof theory
• Confluence of the lambda calculus with left-linear algebraic rewriting
• Confluence and superdevelopments
• Standard and Normal Reductions
• The Equivalence of Complete Reductions
• Rewriting, and equational unification: the higher-order cases
• On the longest perpetual reductions in orthogonal expression reduction systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (68)

• Perpetuality and uniform normalization in orthogonal rewrite systems
• Computing in unpredictable environments: semantics, reduction strategies, and program transformations
• Inductive-data-type systems
• Introducing \(\llparenthesis\lambda\rrparenthesis\), a \(\lambda \)-calculus for effectful computation
• Higher-order interpretations and program complexity
• Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions
• On the Relation between Sized-Types Based Termination and Semantic Labelling
• Matching and alpha-equivalence check for nominal terms
• Infinitary combinatory reduction systems
• Term Rewriting and Applications
• The variable containment problem
• On the confluence of lambda-calculus with conditional rewriting
• Processes, Terms and Cycles: Steps on the Road to Infinity
• Expressing combinatory reduction systems derivations in the rewriting calculus
• A framework for defining logical frameworks
• Higher-order rewrite systems and their confluence
• Title not available (Why is that?)
• Variable binding operators in transition system specifications
• The power of closed reduction strategies
• Size-based termination of higher-order rewriting
• Expression reduction systems with patterns
• Logical foundations for hybrid type-logical grammars
• Nominal Confluence Tool
• Capture-avoiding substitution as a nominal algebra
• Checking overlaps of nominal rewriting rules
• On the longest perpetual reductions in orthogonal expression reduction systems
• Lambda calculus with explicit recursion
• Gödel's system \(\mathcal T\) revisited
• Normalisation for higher-order calculi with explicit substitutions
• A metamodel of access control for distributed environments: applications and properties
• Developing developments
• Intersection type assignment systems with higher-order algebraic rewriting
• Strong normalization from weak normalization in typed \(\lambda\)-calculi
• Order-sorted inductive types
• Strong normalisation in two Pure Pattern Type Systems
• Abstract reduction systems and idea of Knuth-Bendix completion algorithm
• Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
• Nominal rewriting
• A new connective in natural deduction, and its application to quantum computing
• On explicit substitution with names
• Introducing a Calculus of Effects and Handlers for Natural Language Semantics
• Combining algebraic rewriting, extensional lambda calculi, and fixpoints
• Counterexamples in infinitary rewriting with non-fully-extended rules
• Rewriting calculus with(out) types
• Recursive Functions with Pattern Matching in Interaction Nets
• From functional programs to interaction nets via the rewriting calculus
• Axiomatizing permutation equivalence
• Interaction systems II: The practice of optimal reductions
• A prismoid framework for languages with resources
• Token-passing nets for functional languages
• Three Syntactic Theories for Combinatory Graph Reduction
• Theorem proving modulo
• Complete laziness: a natural semantics
• A modular construction of type theories
• On Normalisation of Infinitary Combinatory Reduction Systems
• Comparing Böhm-Like Trees
• Interaction nets and term rewriting systems (extended abstract)
• Descendants and origins in term rewriting.
• Combinatory reduction systems with explicit substitution that preserve strong normalisation
• Title not available (Why is that?)
• Minimal relative normalization in orthogonal expression reduction systems
• Title not available (Why is that?)
• Harnessing First Order Termination Provers Using Higher Order Dependency Pairs
• The algebra of recursive graph transformation language UnCAL: complete axiomatisation and iteration categorical semantics
• On basic feasible functionals and the interpretation method
• Sharing proofs with predicative theories through universe-polymorphic elaboration
• Title not available (Why is that?)
• Labelled reductions, runtime errors, and operational subsumption

Uses Software

• ETPS
• Automath

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)