computations

Basic idea

Models of computation that programming languages can be reduced to or built on top of: $\lambda$-calculus, interaction nets, combinators. They give a precise, machine-independent meaning to “what a program computes” and a cost model for reasoning about it.

Key facts

• $\lambda$-calculus (Church, 1930s): functions and application; Turing-complete; underlies functional languages.
• Interaction nets (Lafont, 1990): graph rewriting with strong confluence; basis of optimal $\lambda$-reducers (HVM).
• Church-Turing thesis: all reasonable models of computation are equivalent in what they can compute (not in cost).

Pages

• Interaction Nets
• lambda

Siblings

• codegen
• optimisations
• parsers
• semantics
• types