## Contributors * Rod Nederpelt * Fairouz Kamareddine * Crispin Wright (neo-Fregean) * Bob Hale (neo-Fregean) * Luitzen Egbertus Jan Brouwer * Arend Heyting ## 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, [web](http://www.cedar-forest.org/forest/projects/AdvNewLamNot.html) * Yves Bertot, Pierre Castéran, Le Coq' Art, 2011, [pdf](http://www.labri.fr/perso/casteran/CoqArt/coqartF.pdf) * Coq manual, [web](http://coq.inria.fr/doc/toc.html) * Coq tutorial, [web](http://coq.inria.fr/V8.1/tutorial.html) * [[type theory]] * 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)