Variable binding and substitution for (nameless) dummies

DOI10.46298/lmcs-20(1:18)2024arXiv2209.02614v6OpenAlexW4392385926MaRDI QIDQ6151566

Tom Hirschowitz, Andre Hirschowitz, Marco Maggesi, Ambroise Lafont

Publication date: 11 March 2024

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2209.02614v6

zbMATH Keywords

category theorysyntaxsubstitutionvariable binding

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Modules over monads and initial semantics
• On the construction of free algebras for equational systems
• Nested abstract syntax in Coq
• A formalized general theory of syntax with bindings: extended version
• Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions
• Coproducts of Monads on Set
• Presentation of Set Functors: A Coalgebraic Perspective
• Modules over Monads and Linearity
• de Bruijn notation as a nested datatype
• Residual theory in λ-calculus: a formal development
• A Cellular Howe Theorem
• Monads need not be endofunctors
• Abstract Syntax: Substitution and Binders
• On monads and warpings
• Theorem Proving in Higher Order Logics

This page was built for publication: Variable binding and substitution for (nameless) dummies