Substitution in non-wellfounded syntax with variable binding

DOI10.1016/J.TCS.2004.07.025MaRDI QIDQ703526zbMATH OpenOpenAlexFDO

Authors Ralph Matthes, Tarmo Uustalu

Publication date 11 January 2005

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

Full work available at URL https://doi.org/10.1016/j.tcs.2004.07.025

zbMATH Keywords

Final coalgebraFunctor categoryMonadNon-wellfounded syntaxPrimitive corecursionSubstitutionVariable binding

Mathematics Subject Classification ID

Categorical semantics of formal languages (18C50) Abstract data types; algebraic specification (68Q65)

Recommendations

• Substitution in non-wellfounded syntax with variable binding
• Explicit substitutions and higher-order syntax
• A formalized general theory of syntax with bindings
• A formalized general theory of syntax with bindings: extended version
• Heterogeneous substitution systems revisited

Cites work

• scientific article; zbMATH DE number 1375587 (Why is no real title available?)
• scientific article; zbMATH DE number 3722625 (Why is no real title available?)
• scientific article; zbMATH DE number 1343506 (Why is no real title available?)
• scientific article; zbMATH DE number 1948154 (Why is no real title available?)
• scientific article; zbMATH DE number 1956505 (Why is no real title available?)
• scientific article; zbMATH DE number 2003147 (Why is no real title available?)
• scientific article; zbMATH DE number 1759453 (Why is no real title available?)
• scientific article; zbMATH DE number 2087341 (Why is no real title available?)
• scientific article; zbMATH DE number 1841846 (Why is no real title available?)
• scientific article; zbMATH DE number 2090071 (Why is no real title available?)
• scientific article; zbMATH DE number 1424053 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• A framework for defining logics
• An algebraic generalization of Frege structures -- binding algebras
• Basic category theory for models of syntax.
• Coalgebraic monads
• Coequalizers and free triples
• Dualising initial algebras
• Explicit substitutions and higher-order syntax
• Generalised folds for nested datatypes
• Generalizing Substitution
• Infinitary lambda calculus
• Infinite trees and completely iterative theories: A coalgebraic view
• Locus solum: From the rules of logic to the logic of rules.
• Parametric corecursion
• Proceedings of the seventh ACM SIGPLAN international conference on Functional programming
• Reduction of finite and infinite derivations
• Substitution in non-wellfounded syntax with variable binding
• Substitution: A formal methods case study using monads and transformations
• de Bruijn notation as a nested datatype

Cited in

(18)

• From signatures to monads in \textsf{UniMath}
• Generalizing Substitution
• Substitution in non-wellfounded syntax with variable binding
• Lazy variable-renumbering makes substitution cheap
• Explicit substitutions and higher-order syntax
• A formalized general theory of syntax with bindings
• Structured handling of scoped effects
• High-level signatures and initial semantics
• Some Wellfounded Trees in UniMath
• C-system of a module over a \(Jf\)-relative monad
• Modules over monads and initial semantics
• Unifying structured recursion schemes. An extended study
• Substitution for non-wellfounded syntax with binders through monoidal categories
• Towards Effects in Mathematical Operational Semantics
• scientific article; zbMATH DE number 7379288 (Why is no real title available?)
• Heterogeneous substitution systems revisited
• scientific article; zbMATH DE number 5360218 (Why is no real title available?)
• Coproducts of Ideal Monads

This page was built for publication: Substitution in non-wellfounded syntax with variable binding

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