Metric Reasoning about $\lambda$-Terms: the Affine Case (Long Version)

Raphaëlle Crubillé, Ugo Dal Lago

Terms of Church's $\lambda$-calculus can be considered equivalent along many different definitions, but context equivalence is certainly the most direct and universally accepted one. If…