Articulating the ineffable. Programming language theory 
cognitive psychology. PhD @Stanford
You can add location information to your Tweets, such as your city or precise location, from the web and via third-party applications. You always have the option to delete your Tweet location history. Learn more
Curry-Howard correspondence! :) I would recommend Wadler’s Types as Propositions for this, only because there is no other better paper.
I understand Curry-Howard in the abstract, but it doesn't seem to be the full picture. e.g. CHC is usually explained as correspondences between functional programs and constructive logic, incl. warnings against excluded middle. But in Lean, I can just call "classical.em". Why?
I have not used Lean. Including LEM is sometimes necessary to be able to give it to a SAT solver perhaps? I am no expert here, there are other who may be able you answer your questions better. :)
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.
