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
- Entry for William Alvin Howard at the Mathematics Genealogy Project.
- Howard, W. A.; Kreisel, G. (Sep 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.