Sharing Equality is Linear
Andrea Condoluci, Beniamino Accattoli, Claudio Sacerdoti Coen · 2019
The λ-calculus is a handy formalism to specify the evaluation of higher-order programs. It is not very handy, however, when one interprets the specification as an execution mechanism, because terms can grow exponentially with the number of β-steps. This is why implementations of functional languages and proof assistants always rely on some form of sharing of subterms.