## Contributors * Friedrich Ludwig Gottlob Frege (modern logic, analytic philosophy) * David Hilbert (Hilbert's program, formalism, ''computabilism'') * Bertrand Russell (type theory of the ''principia mathematica'') * (see the numerous contributors to type theory) * Ernst Zermelo (axiomatic set theory) * Luitzen Egbertus Jan Brouwer (intuitionistic mathematics) * Arend Heyting * Abraham Fraenkel (Zermelo-Fraenkel set theory) * Kurt Friedrich Gödel (completeness theorem, incompleteness theorem) * Alan Turing (proof that the halting problem is not solvable; this recovers Gödel's incompleteness theorem from computational viewpoint. Turing machine; this is a model for computation) * Willard Van Orman Quine (new foundations; this is a type theory) * Samuel Eilenberg, Saunders Mac Lane (category theory; however it was argued by others that category theory is a foundational theory; see e.g. [this](http://www.math.mcgill.ca/rags/seminar/Marquis_KreiselLawvere.pdf)) * Francis William Lawvere (category theory, topos theory) * Crispin Wright (neo-Fregean) * Bob Hale (neo-Fregean) * Vladimir Voevodsky (homotopy type theory and univalent foundations) * Harvey Friedman (reverse mathematics) * Rod Nederpelt (weak type theory; related to natural language semantics) * Fairouz Kamareddine ## References * Rod Nederpelt, weak type theory: a formal language for mathematics, [pdf](http://alexandria.tue.nl/extra1/wskrap/publichtml/200205.pdf) * EPSRC project- Theoretical and Implementation advantages of a new lambda notation, (on Automath), [web](http://www.cedar-forest.org/forest/projects/AdvNewLamNot.html) * [[Coq]] * Freek Wiedijk, the QED manifesto revisited, Nijmegen, 2007, [pdf](http://mizar.org/trybulec65/8.pdf) * A foundation for metareasoning part II: the [[model theory]], [pdf](http://www.mi.sanu.ac.rs/~uros.m/logcom/hdb/Volume_12/Issue_03/pdf/120345.pdf) * homotopy type theory and univalent foundations, [web](http://homotopytypetheory.org) * [[type theory]] * Steward Shapiro: Foundations without Foundationalism: A Case for Second-order Logic, 2000