The problem is to find the typing derivation of a term of the call-by-value STLC extended with reference types. The evaluation and typing rules for this language is given in Types and Programming Languages by Pierce on page 166. The term is $ $ t = (\lambda a:\mathrm{Ref}\mathrm{Bool}. \mathrm{if}\, \mathrm{true}\,\mathrm{then}\, !l_1\, !a\, \mathrm{else}\,0)\,\mathrm{ref}\,\mathrm{true} $ $ where $ $ \mu(l_1)=\lambda x:\mathrm{Int}.x $ $ So I need to find $ \Gamma, \Sigma,$ and $ T$ so that $ $ \Gamma\,|\,\Sigma\vdash t:T $ $ I know you are supposed to show your work, but my problem is that $ t$ doesn’t seem well-typed… What am I missing?