Substitution in non-wellfounded syntax with variable binding

DOI10.1016/j.tcs.2004.07.025zbMath1071.68063MaRDI QIDQ703526

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 coalgebra; Functor category; Monad; Non-wellfounded syntax; Primitive corecursion; Substitution; Variable binding

Mathematics Subject Classification ID

68Q65: Abstract data types; algebraic specification

18C50: Categorical semantics of formal languages

Related Items

Unnamed Item, Generalizing Substitution, Coproducts of Ideal Monads, Unnamed Item, Unifying structured recursion schemes, Towards Effects in Mathematical Operational Semantics, Semantics of Higher-Order Recursion Schemes, Modules over monads and initial semantics, From signatures to monads in \textsf{UniMath}, Some Wellfounded Trees in UniMath

Cites Work

• Explicit substitutions and higher-order syntax
• An algebraic generalization of Frege structures -- binding algebras
• Substitution: A formal methods case study using monads and transformations
• Infinitary lambda calculus
• Infinite trees and completely iterative theories: A coalgebraic view
• Reduction of finite and infinite derivations
• Generalised folds for nested datatypes
• Coequalizers and free triples
• Locus Solum: From the rules of logic to the logic of rules
• Coalgebraic Monads
• A framework for defining logics
• de Bruijn notation as a nested datatype
• Dualising initial algebras
• Generalizing Substitution
• Generic Programming
• Proceedings of the seventh ACM SIGPLAN international conference on Functional programming
• Parametric corecursion
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item