Substitution in non-wellfounded syntax with variable binding

DOI10.1016/j.tcs.2004.07.025zbMath1071.68063OpenAlexW2130486716MaRDI 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 coalgebraFunctor categoryMonadNon-wellfounded syntaxPrimitive corecursionSubstitutionVariable binding

Mathematics Subject Classification ID

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

Related Items (13)

Structured handling of scoped effects ⋮ C-system of a module over a \(Jf\)-relative monad ⋮ Unnamed Item ⋮ Unifying structured recursion schemes ⋮ Modules over monads and initial semantics ⋮ Coproducts of Ideal Monads ⋮ Towards Effects in Mathematical Operational Semantics ⋮ Semantics of Higher-Order Recursion Schemes ⋮ High-level signatures and initial semantics ⋮ Some Wellfounded Trees in UniMath ⋮ Generalizing Substitution ⋮ From signatures to monads in \textsf{UniMath} ⋮ Heterogeneous Substitution Systems Revisited

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

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