scientific article
From MaRDI portal
Publication:3918095
zbMath0466.03006MaRDI QIDQ3918095
Publication date: 1980
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Combinatory logic and lambda calculus (03B40)
Related Items
Context rewriting, A categorical formulation for critical-pair/completion procedures, Extended term rewriting systems, Testing confluence of nonterminating rewriting systems, Uniqueness of Normal Forms for Shallow Term Rewrite Systems, Optimal reductions in interaction systems, Classes of equational programs that compile into efficient machine code, Adding algebraic rewriting to the untyped lambda calculus (extended abstract), On confluence for weakly normalizing systems, Open problems in rewriting, More problems in rewriting, A termination ordering for higher order rewrite systems, Proving the genericity lemma by leftmost reduction is simple, Problems in rewriting III, Combinatory reduction systems with explicit substitution that preserve strong normalisation, Higher-order families, Unique normal forms for nonlinear term rewriting systems: Root overlaps, Complete algebraic semantics for second-order rewriting systems based on abstract syntax with variable binding, Higher order conditional rewriting and narrowing, Tight typings and split bounds, fully developed, Unnamed Item, Decreasing diagrams with two labels are complete for confluence of countable systems, A confluent reduction for the extensional typed λ-calculus with pairs, sums, recursion and terminal object, Combining first order algebraic rewriting systems, recursion and extensional lambda calculi, R n - and G n -logics, The variable containment problem, Development closed critical pairs, Term Equational Systems and Logics, The dynamics of information exchange dialogues, Unique normal form property of compatible term rewriting systems: A new proof of Chew's theorem, Explicit substitutions, Inductive-data-type systems, Weak normalization implies strong normalization in a class of non-dependent pure type systems, On the longest perpetual reductions in orthogonal expression reduction systems, Strong Normalisation of Cut-Elimination That Simulates β-Reduction, Unnamed Item, Transfinite reductions in orthogonal term rewriting systems, Unnamed Item, Unnamed Item, The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type, Theoretical Pearl Yet yet a counterexample for λ+SP, Redexes are stable in the λ-calculus, Higher-order narrowing with definitional trees, Computing in unpredictable environments: Semantics, reduction strategies, and program transformations, Effective longest and infinite reduction paths in untyped λ-calculi, Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs, An extension of Klop's counterexample to the Church-Rosser property to \(\lambda\)-calculus with other ordered pair combinators, Eta-conversion for the languages of explicit substitutions, Possible forms of evaluation or reduction in Martin-Löf type theory, Reduction and unification in lambda calculi with a general notion of subtype, Parametric parameter passing \(\lambda\)-calculus, Needed reduction and spine strategies for the lambda calculus, Combining algebraic rewriting, extensional lambda calculi, and fixpoints, Interaction systems II: The practice of optimal reductions, The Prismoid of Resources, Converting between Combinatory Reduction Systems and Big Step Semantics, A higher-order calculus and theory abstraction, An initial algebra approach to term rewriting systems with variable binders, One-step recurrent terms in \(\lambda\)-\(\beta\)-calculus, Normal forms in combinatory logic, NP-completeness of a combinator optimization problem, Expressing combinatory reduction systems derivations in the rewriting calculus, Counterexamples to termination for the direct sum of term rewriting systems, A formal algorithmic language FALGOL. Thirty years after, Comparing cubes of typed and type assignment systems, Conditional rewrite rules: Confluence and termination, Unique normal forms for lambda calculus with surjective pairing, On the Jacopini technique, The geometry of orthogonal reduction spaces, Resource operators for \(\lambda\)-calculus, Lambda calculus with explicit recursion, Higher-order rewrite systems and their confluence, A \(\rho\)-calculus of explicit constraint application, A notation for lambda terms. A generalization of environments, Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters, Infinitary rewriting: meta-theory and convergence, A Confluent Rewriting System Having No Computable, One-Step, Normalizing Strategy, From diagrammatic confluence to modularity, Highlights in infinitary rewriting and lambda calculus, Interaction nets and term-rewriting systems, Computing in unpredictable environments: semantics, reduction strategies, and program transformations, A confluent calculus for concurrent constraint programming, Developing developments, Towards ``mouldable code via nested code graph transformation, Braids via term rewriting, Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility, A type-assignment of linear erasure and duplication, A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names., Spinal atomic \(\lambda\)-calculus, Böhm theorem and Böhm trees for the \(\varLambda \mu\)-calculus, A rationale for conditional equational programming, Confluence results for the pure strong categorical logic CCL. \(\lambda\)- calculi as subsystems of CCL, Lambda calculus with patterns, On strong normalization and type inference in the intersection type discipline, Three Syntactic Theories for Combinatory Graph Reduction, On the expressive power of finitely typed and universally polymorphic recursive procedures, A criterion for proving noetherianity of a relation, A sequential reduction strategy, Transformations and confluence for rewrite systems, A combinatory logic approach to higher-order E-unification, Conditional rewriting logic as a unified model of concurrency, Programs as data structures in \(\lambda\)SF-calculus, Expression reduction systems with patterns, Strong normalization through intersection types and memory, On abstract normalisation beyond neededness, Confluence of the lambda calculus with left-linear algebraic rewriting, A theory of binding structures and applications to rewriting, Adding algebraic rewriting to the untyped lambda calculus, Capturing strong reduction in director string calculus, How to decide the lark, De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: The typed case, Conditional linearization, De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: the untyped case, On equal \(\mu \)-terms, New proofs of important theorems of untyped extensional \(\lambda\) calculus, Infinitary combinatory reduction systems, Normalisation for higher-order calculi with explicit substitutions, On the confluence of lambda-calculus with conditional rewriting, A proof of the leftmost reduction theorem for \(\lambda\beta\eta\)-calculus, First-class patterns, Theory and practice of second-order rewriting: foundation, evolution, and SOL, Functional pearl: the distributive \(\lambda\)-calculus, De Bruijn's weak diamond property revisited, Term-rewriting systems with rule priorities, Diagram techniques for confluence, Explicit substitution. On the edge of strong normalization, Orders, reduction graphs and spectra, Sequential evaluation strategies for parallel-or and related reduction systems, Perpetual reductions in \(\lambda\)-calculus, The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective), Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions, Linear numeral systems, (In)efficiency and reasonable cost models, Reduction graphs in the lambda calculus, The algebra of recursive graph transformation language UnCAL: complete axiomatisation and iteration categorical semantics, Partial completion of equational theories, Algorithms and reductions for rewriting problems. II., Descendants and origins in term rewriting., Perpetuality and uniform normalization in orthogonal rewrite systems, A characterization of weakly Church-Rosser abstract reduction systems that are not Church-Rosser, Conservation and uniform normalization in lambda calculi with erasing reductions, The conflict-free reduction geometry, Structuring Operational Semantics: Simplification and Computation, Combinatory reduction systems: Introduction and survey, Complete Laziness: a Natural Semantics, Relating conflict-free stable transition and event models via redex families
