The local reference τ& y = e binds a second name to the location e denotes, without allocating.

The initialiser must denote a location and have the declared type, and the reference has in \Gamma the type of its referent, because every read and write through it is a read or write at the referent.

The binding is an alias, not owned, so the exit of the block that declared the reference leaves the location in \sigma.

A reference to a temporary, to nullptr or to an expression without a location does not exist, and a dangling reference is impossible by construction, because a reference names only locations of enclosing blocks or of objects in the store.

\dfrac{\Gamma \vdash_{\ell} e : \tau \qquad \tau \text{ has values}}{\Gamma \vdash \tau\mathtt{\&}\ x = e \dashv \Gamma[x \mapsto \tau]}\;\textsf{(T-DeclRef)}

\dfrac{\rho, \sigma \vdash e \Rightarrow_{\ell} \ell, \sigma'}{\rho, \sigma \vdash \tau\mathtt{\&}\ x = e \Rightarrow \mathsf{normal}, \rho[x \mapsto \ell], \sigma'}\;\textsf{(DeclRef)}

Some of the implementations are partial, so Lean records opaque constants that carry the type and not the body, and no property of them is proved here.