The Semantics and Implementation of Bindings in Higher-Order Programming Languages

A fundamental activity in programming language design is the association of a name to a syntactic phrase. This is called a definition binding, since the name defines the syntactic phrase. Bindings can also arise as a consequence of parameter transmission, via the association of a formal parameter name to an actual parameter, and are termed parameter bindings. Bindings can be understood in many different ways: we study two popular semantics of bindings, namely, eager (or call-by-value) semantics and lazy (or call-by-name) semantics. We validate Landin's correspondence principle, a benchmark of programming language design, by developing a categorical model for a higher-order, modular language. The model provides a uniform semantics of definition and parameter bindings. If the language satisfies the correspondence principle, the categorical model is a weakly symmetric, monoidal-closed category. This allows the understanding of definitions as records, their invocation as record indexing, ..