Many models of (differential) linear logic and lambda-calculus can be regarded as a quantitative enrichment of the relational semantics of linear logic. This talk presents an introduction to these models, taking a simple but flexible approach. Relations can be enriched with coefficients drawn from any complete semiring — a structure which allows multiplication and infinite summation of quantities — and in each case we obtain a soundness result with respect to a quantitative operational semantics for a functional language with recursion, nondeterminism and quantitative effects. Examples include models that track the number of possible reduction paths, the length of the shortest reduction path, or the probability of termination of a program.[-]

Geometry of Interaction, combined with translation of lambda-calculus into MELL proof nets, has enabled an unconventional approach to program semantics. Danos and Regnier, and Mackie pioneered the approach, and introduced the so-called token-passing machines.
It turned out that the unconventional token-passing machines can be turned into a graphical realisation of conventional reduction semantics, in a simple way. The resulting semantics can be more convenient than the standard (syntactical) reduction semantics, in analysing local behaviour of programs. I will explain how, in particular, the resulting graphical reduction semantics can be used to reason about observational equivalence between programs.[-]