Quantitative semantics

We shall present a quantitative denotational semantics of the typed lambda-calculus and of linear logic where formulae are interpreted by vector spaces and proofs by vectors. This interpretation, which is based on a very simple notion of finiteness space that we shall introduce, avoids all topological considerations, and can be considered as purely algebraic. We shall see that it gives rise to an extension of logic (and functional languages) by differential constructs which are deeply linked to the notion of "linear substitution".