William Alvin Howard

From Wikipedia, the free encyclopedia

William Alvin Howard (1926 -) is a proof theorist most well-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 has also been active in the theory of proof-theoretic ordinals. He earned his Ph.D. at the University of Chicago in 1956.

The Howard ordinal or Bachmann-Howard ordinal was named after him.

[edit] External links

Languages