A typechecker and interpreter for the linear lambda calculus as presented in the Pfenning course on linear logic