git @ Cat's Eye Technologies The-Glosscubator / master by-topic / Name Binding
master

Tree @master (Download .tar.gz)

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. β˜… πŸ’­

bacam/sato-maps-agda β˜… πŸ’­

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 β˜… πŸ’­

Viewing Ξ»-terms through Maps

A nominal axiomatisation of the lambda-calculus

Second-Order and Dependently-Sorted Abstract Syntax

(in Lambda Calculus) A Lambda Calculus with Naive Substitution (online @ www.cambridge.org) πŸ’­

(in Term Rewriting) Combinatory Reduction Systems β˜…β˜… πŸ’­

(in Term Rewriting) Matching Power β˜… πŸ’­

History of by-topic / Name Binding @master git clone https://git.catseye.tc/The-Glosscubator/