A theory of binding structures and applications to rewriting

DOI10.1016/0304-3975(93)90240-TzbMath0783.68089OpenAlexW1995328923MaRDI QIDQ685380

Carolyn L. Talcott

Publication date: 17 October 1993

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

Full work available at URL: https://doi.org/10.1016/0304-3975(93)90240-t

zbMATH Keywords

homomorphismsunificationrewritingalgebra of binding structuresfirst-order reasoningstructural recursion

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Applications of universal algebra in computer science (08A70) Data structures (68P05) Theory of computing (68Q99)

Related Items

An initial algebra approach to term rewriting systems with variable binders, Labelled reductions, runtime errors, and operational subsumption, A lambda-calculus for dynamic binding, A first order logic of effects, A typed context calculus, Axiomatizing permutation equivalence, Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables, A practical implementation of simple consequence relations using inductive definitions, Higher-order substitutions, Combinatory reduction systems: Introduction and survey

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Notions of computation and monads
• The lambda calculus, its syntax and semantics
• Algebraic construction of compilers
• Inferring the equivalence of functional programs that mutate data
• Proving and applying program transformations expressed with second-order patterns
• On the algebraic definition of programming languages
• Equivalence in functional languages with effects
• A logic programming language with lambda-abstraction, function variables, and simple unification
• Algebras with a Scheme of Operators