Combinatory reduction systems: Introduction and survey
From MaRDI portal
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)
