A theory of binding structures and applications to rewriting

DOI10.1016/0304-3975(93)90240-TMaRDI QIDQ685380zbMATH OpenOpenAlexFDO

Authors Carolyn 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

rewritinghomomorphismsunificationalgebra of binding structuresfirst-order reasoningstructural recursion

Mathematics Subject Classification ID

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

Recommendations

• Fundamentals of compositional rewriting theory
• Automata, Languages and Programming
• A formalized general theory of syntax with bindings
• Structures for abstract rewriting
• A rewriting approach to the combination of data structures with bridging theories
• A formalized general theory of syntax with bindings: extended version
• Publication:4938613
• Pullback rewriting and applications
• scientific article; zbMATH DE number 1118018
• Infinitary rewriting: foundations revisited

Cites work

• scientific article; zbMATH DE number 3730111 (Why is no real title available?)
• scientific article; zbMATH DE number 8800 (Why is no real title available?)
• scientific article; zbMATH DE number 89006 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• A logic programming language with lambda-abstraction, function variables, and simple unification
• Algebraic construction of compilers
• Algebras with a Scheme of Operators
• Equivalence in functional languages with effects
• Inferring the equivalence of functional programs that mutate data
• Notions of computation and monads
• On the algebraic definition of programming languages
• Proving and applying program transformations expressed with second-order patterns
• The lambda calculus, its syntax and semantics

Cited in

(13)

• A practical implementation of simple consequence relations using inductive definitions
• A first order logic of effects
• A lambda-calculus for dynamic binding
• An initial algebra approach to term rewriting systems with variable binders
• A typed context calculus
• Combinatory reduction systems: Introduction and survey
• Higher-order substitutions
• Theory and practice of second-order rewriting: foundation, evolution, and SOL
• scientific article; zbMATH DE number 1476647 (Why is no real title available?)
• Axiomatizing permutation equivalence
• Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables
• Labelled reductions, runtime errors, and operational subsumption
• Pullback rewriting and applications

This page was built for publication: A theory of binding structures and applications to rewriting

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q685380)