William Alvin Howard
From Wikipedia, the free encyclopedia
William Alvin Howard (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 has also been active in the theory of proof-theoretic 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 or Bachmann-Howard ordinal was named after him.
[edit] External links
- Entry for William Alvin Howard at the Mathematics Genealogy Project.
- Howard, W. A.; Kreisel, G. (September 1966). "Transfinite Induction and Bar Induction of Types Zero and One, and the Role of Continuity in Intuitionistic Analysis". The Journal of Symbolic Logic 3 (3): 325–358. doi:. http://links.jstor.org/sici?sici=0022-4812%28196609%2931%3A3%3C325%3ATIABIO%3E2.0.CO%3B2-7&size=LARGE.

