Name Binding
(Up) | See also: Lambda Calculus, Theorem Proving
Web resources
How do real-world proof assistants bind variables and check equality? ★
Repositories
mathink/mslambda: Map, Skeleton, Lambda term. ★ 💭
jsiek/abstract-binding-trees: Abstract binding trees (abstract syntax trees plus binders), as a library in Agda ★ 💭
Papers
Foundational Aspects of Syntax (online @ web.archive.org) ★ 💭
Abstract Syntax for Variable Binders (online @ web.archive.org) ★ 💭
A Simple Take on Typed Abstract Syntax in Haskell-like Languages (online @ tidsskrift.dk) ★ 💭
A Metalanguage for Programming with Bound Names Modulo Renaming
I am not a Number, I am a Free Variable ★ 💭
A Type and Scope Safe Universe of Syntaxes with Binding
Five Axioms of Alpha-Conversion ★
Don’t Substitute Into Abstractions (Functional Pearl)
Abstract Binding Trees, Dynamics and Statics ★ 💭
(in Lambda Calculus) A Lambda Calculus with Naive Substitution (online @ www.cambridge.org) 💭
(in Term Rewriting) Combinatory Reduction Systems ★★ 💭
(in Term Rewriting) Matching Power ★ 💭