We develop a theory of abstract syntax with variableudbinding. To every binding signature we associate a categoryudof models consisting of variable sets endowed withudcompatible algebra and substitution structures. The syntaxudgenerated by the signature is the initial model. This gives audnotion of initial algebra semantics encompassing the traditionaludone; besides compositionality, it automatically veri-udfies the semantic substitution lemma.
展开▼
