The correctness of a modified SECD machine
Clement L. McGowan · 1970
Landin's SECD Machine does not completely compute certain expressions of the λ-calculus and so is modified by the addition of an output component and a unique name counter. This modified machine is proven to correctly implement the λ-calculus.