Name: Anonymous 2013-03-18 12:50
Nominated for this months programer spotlight: http://www.reddit.com/user/tactics
his interests are dependent type theory (an advanced version of haskell where you can write proofs), an has become a self-taught mathematician so that he can evangelize the future: "homotopy type theory" to the mathematicians of reddit.
Selected Quotes:
Can I get some dependent types up in here?
What problems don't dependent types solve? :)
Under the Curry Howard Correspondence ....
And his magnum opus "Don't forget Homotopy Type Theory." http://www.reddit.com/r/math/comments/17nvlr/zermelofraenkel_set_theory_peano_arithmetic/c87cqb3
his interests are dependent type theory (an advanced version of haskell where you can write proofs), an has become a self-taught mathematician so that he can evangelize the future: "homotopy type theory" to the mathematicians of reddit.
Selected Quotes:
Can I get some dependent types up in here?
What problems don't dependent types solve? :)
Under the Curry Howard Correspondence ....
And his magnum opus "Don't forget Homotopy Type Theory." http://www.reddit.com/r/math/comments/17nvlr/zermelofraenkel_set_theory_peano_arithmetic/c87cqb3