William Alvin Howard

William Alvin Howard (born 1926) is a proof theorist best known for his work demonstrating formal similarity between intuitionistic logic and the simply typed lambda calculus that has come to be known as the Curry–Howard correspondence.

He earned his Ph.D. at the University of Chicago in 1956 for his dissertation "k-fold recursion and well-ordering".

[1] He was a student of Saunders Mac Lane.

He was the first to carry out an ordinal analysis of the intuitionistic theory

[2]p.27 He was elected to the 2018 class of fellows of the American Mathematical Society.