Combinatory reduction systems: Introduction and survey
From MaRDI portal
Publication:1314356
DOI10.1016/0304-3975(93)90091-7zbMath0796.03024OpenAlexW4212868911MaRDI QIDQ1314356
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
confluenceterm rewriting systemslambda calculuscombinatory reduction systemsextension of the finite developments theorem
Related Items
A modular construction of type theories ⋮ Higher-order interpretations and program complexity ⋮ Introducing \(\llparenthesis\lambda\rrparenthesis\), a \(\lambda \)-calculus for effectful computation ⋮ Logical foundations for hybrid type-logical grammars ⋮ Nominal rewriting ⋮ Harnessing First Order Termination Provers Using Higher Order Dependency Pairs ⋮ Combinatory reduction systems with explicit substitution that preserve strong normalisation ⋮ Combining algebraic rewriting, extensional lambda calculi, and fixpoints ⋮ Strong normalization from weak normalization in typed \(\lambda\)-calculi ⋮ Expressing combinatory reduction systems derivations in the rewriting calculus ⋮ On explicit substitution with names ⋮ Labelled reductions, runtime errors, and operational subsumption ⋮ Size-based termination of higher-order rewriting ⋮ Lambda calculus with explicit recursion ⋮ Higher-order rewrite systems and their confluence ⋮ Computing in unpredictable environments: semantics, reduction strategies, and program transformations ⋮ Developing developments ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility ⋮ Counterexamples in infinitary rewriting with non-fully-extended rules ⋮ Strong normalisation in two Pure Pattern Type Systems ⋮ On Normalisation of Infinitary Combinatory Reduction Systems ⋮ A metamodel of access control for distributed environments: applications and properties ⋮ A prismoid framework for languages with resources ⋮ Theorem proving modulo ⋮ Capture-avoiding substitution as a nominal algebra ⋮ Intersection type assignment systems with higher-order algebraic rewriting ⋮ Expression reduction systems with patterns ⋮ Checking overlaps of nominal rewriting rules ⋮ The variable containment problem ⋮ Gödel's system \(\mathcal T\) revisited ⋮ Recursive Functions with Pattern Matching in Interaction Nets ⋮ Variable binding operators in transition system specifications ⋮ Unnamed Item ⋮ Infinitary combinatory reduction systems ⋮ Normalisation for higher-order calculi with explicit substitutions ⋮ Matching and alpha-equivalence check for nominal terms ⋮ Unnamed Item ⋮ On the confluence of lambda-calculus with conditional rewriting ⋮ Inductive-data-type systems ⋮ On the longest perpetual reductions in orthogonal expression reduction systems ⋮ A new connective in natural deduction, and its application to quantum computing ⋮ Nominal Confluence Tool ⋮ Axiomatizing permutation equivalence ⋮ Comparing Böhm-Like Trees ⋮ On the Relation between Sized-Types Based Termination and Semantic Labelling ⋮ Introducing a Calculus of Effects and Handlers for Natural Language Semantics ⋮ Order-sorted inductive types ⋮ Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions ⋮ The algebra of recursive graph transformation language UnCAL: complete axiomatisation and iteration categorical semantics ⋮ Descendants and origins in term rewriting. ⋮ Perpetuality and uniform normalization in orthogonal rewrite systems ⋮ 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 ⋮ Interaction nets and term rewriting systems (extended abstract)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A theory of binding structures and applications to rewriting
- Modular properties of conditional term rewriting systems
- The lambda calculus. Its syntax and semantics. Rev. ed.
- A complete inference system for a class of regular behaviours
- Unique normal forms for lambda calculus with surjective pairing
- Confluence of the lambda calculus with left-linear algebraic rewriting
- LCF considered as a programming language
- Sequential evaluation strategies for parallel-or and related reduction systems
- Combinators, \(\lambda\)-terms and proof theory
- Pairing Without Conventional Restraints
- The Equivalence of Complete Reductions
- Standard and Normal Reductions
- Rewriting, and equational unification: the higher-order cases
- Confluence and superdevelopments
- Parallel reductions in \(\lambda\)-calculus
- On the longest perpetual reductions in orthogonal expression reduction systems
- The Clausal Theory of Types
