William Alvin Howard
From Wikipedia, the free encyclopedia
William Alvin Howard is a proof theorist most well-known for his work demonstrating formal similarity between intuitionistic logic and the typed lambda-calculus that has come to be known as the Curry-Howard correspondence. He has also been active in the theory of proof-theoretic ordinals. He earned his Ph.D. at the University of Chicago in 1965.
The Howard ordinal or Bachmann-Howard ordinal was named after him.