From Surf Wiki (app.surf) — the open knowledge base

William Alvin Howard

Quality 0.00 · 0 views · Updated 7 days ago

William Alvin Howard (born 1926) is an American mathematician and 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 has also been active in the theory of proof-theoretic ordinals. He earned his Ph.D. at the University of Chicago in 1956 for his dissertation "k-fold recursion and well-ordering". He was a student of Saunders Mac Lane.