## Contributors * Rod Nederpelt * Fairouz Kamareddine * Crispin Wright (neo-Fregean) * Bob Hale (neo-Fregean) * Luitzen Egbertus Jan Brouwer * Arend Heyting * Vladimir Voevodsky ## 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]]