William Alvin Howard (born 1926) is a proof theorist bestknown for his work demonstrating formal similarity between intuitionistic logic and the simplytyped lambdacalculus that has come to be known as the CurryHoward correspondence. He has also been active in the theory of prooftheoretic ordinals. He earned his Ph.D. at the University of Chicago in 1956, where he was a student of Saunders Mac Lane.
The Howard ordinal (also known as the BachmannHoward ordinal) was named after him.
