Substitution in non-wellfounded syntax with variable binding

DOI10.1016/J.TCS.2004.07.025zbMATH Open1071.68063OpenAlexW2130486716MaRDI QIDQ703526FDOQ703526

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

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

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)

Cites Work

• Infinite trees and completely iterative theories: A coalgebraic view
• Coequalizers and free triples
• A framework for defining logics
• Locus solum: From the rules of logic to the logic of rules.
• Generalizing Substitution
• Parametric corecursion
• Title not available (Why is that?)
• An algebraic generalization of Frege structures -- binding algebras
• Infinitary lambda calculus
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Substitution: A formal methods case study using monads and transformations
• Generalised folds for nested datatypes
• de Bruijn notation as a nested datatype
• Title not available (Why is that?)
• Title not available (Why is that?)
• Dualising initial algebras
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Reduction of finite and infinite derivations
• Coalgebraic monads
• Substitution in non-wellfounded syntax with variable binding
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Basic category theory for models of syntax.
• Proceedings of the seventh ACM SIGPLAN international conference on Functional programming
• Explicit substitutions and higher-order syntax

Cited In (17)

• 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
• Towards Effects in Mathematical Operational Semantics
• Title not available (Why is that?)
• Heterogeneous substitution systems revisited
• Title not available (Why is that?)
• 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)