William Alvin Howard

William Alvin Howard (born 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 for a dissertation entitled "k-fold recursion and well-ordering".^[1] He was a student of Saunders Mac Lane.

The Howard ordinal (also known as the Bachmann–Howard ordinal) was named after him.

References

↑ "Holdings: k-fold recursion and well-ordering". The University of Chicago Library Catalog. Retrieved 2015-05-04.

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 (Association for Symbolic Logic) 3 (3): 325–358. doi:10.2307/2270450. JSTOR 2270450.

This article is issued from Wikipedia - version of the Monday, February 15, 2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.