Hacker News
- Seemingly impossible functional programs (2007) http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/ 45 comments
- Representations of Uncomputable and Uncountable Sets (2008) http://math.andrej.com/2008/02/06/representations-of-uncomputable-and-uncountable-sets/ 9 comments
- The Dawn of Formalized Mathematics http://math.andrej.com/2021/06/24/the-dawn-of-formalized-mathematics/ 58 comments
- Two dozen mathematicians wrote a 600 page book in 6 months on GitHub http://math.andrej.com/2013/06/20/the-hott-book/ 98 comments
- Python’s lambda is broken http://math.andrej.com/2009/04/09/pythons-lambda-is-broken/ 35 comments
Lobsters
- A general definition of dependent type theories http://math.andrej.com/2020/09/14/a-general-definition-of-dependent-type-theories/ 2 comments plt
- The new and improved programming languages zoo http://math.andrej.com/2016/09/07/the-new-and-improved-programming-languages-zoo/ 5 comments compilers , compsci , ml
- [blog] Mathematics and Computation | A general definition of dependent type theories http://math.andrej.com/2020/09/14/a-general-definition-of-dependent-type-theories/ 5 comments compsci
- On complete ordered fields http://math.andrej.com/2019/09/09/on-complete-ordered-fields/ 7 comments math
- Derivations as computations, by Andrej Bauer: "we think of a derivation as a computation tree showing how to compute its conclusion." [abstract + link to PDF of slides] http://math.andrej.com/2019/08/21/derivations-as-computations/ 4 comments compsci
- "What is an explicit bijection?", by Andrej Bauer. "I shall not give you the definitive answer ... but will give *an* answer, and along the way we will see how foundations can shape our understanding of mathematics." [PDF of slides] http://math.andrej.com/wp-content/uploads/2019/07/what-is-an-explicit-bijection-fpsac-2019-slides-with-presenter-notes.pdf 13 comments math
- Blog post: "Free variables are not 'implicitly universally quantified'!" http://math.andrej.com/2012/12/25/free-variables-are-not-implicitly-universally-quantified/ 16 comments math
- Constructive mathematics: reading list? http://math.andrej.com/2010/03/29/proof-of-negation-and-proof-by-contradiction/ 20 comments math
- Proof of negation and proof by contradiction http://math.andrej.com/2010/03/29/proof-of-negation-and-proof-by-contradiction/ 64 comments math
- An injection from Baire space to natural numbers http://math.andrej.com/2011/06/15/constructive-gem-an-injection-from-baire-space-to-natural-numbers/ 9 comments math
- "The Programming languages Zoo, a potpourri of miniature but fully functioning programming language implementations ... demonstrate[s] design and implementation techniques, from dirty practical details to lofty theoretical considerations" http://math.andrej.com/2016/09/07/the-new-and-improved-programming-languages-zoo/ 13 comments compsci
- The new and improved Programming languages zoo http://math.andrej.com/2016/09/07/the-new-and-improved-programming-languages-zoo/ 11 comments ocaml
- The new and improved Programming languages zoo http://math.andrej.com/2016/09/07/the-new-and-improved-programming-languages-zoo/ 6 comments programming
- Formal proofs are not just deduction steps http://math.andrej.com/2016/08/30/formal-proofs-are-not-just-deduction-steps/ 7 comments math
- Hask is not a category http://math.andrej.com/2016/08/06/hask-is-not-a-category/ 46 comments haskell
- Hask is not a category http://math.andrej.com/2016/08/06/hask-is-not-a-category/ 26 comments programming
- Apparently impossible functional programs. http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/ 24 comments programming
- Seemingly impossible functional programs http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/ 15 comments haskell
- Univalent foundations subsume classical mathematics (xpost from /r/Dependent_Types) http://math.andrej.com/2014/01/13/univalent-foundations-subsume-classical-mathematics/ 6 comments math
- The Elements of an Inductive Type http://math.andrej.com/2013/08/28/the-elements-of-an-inductive-type/ 29 comments haskell
- Synthetic differential geometry, advertized as "intuitionistic math for physics". http://math.andrej.com/2008/08/13/intuitionistic-mathematics-for-physics/ 34 comments math
- AskMath: Current state of formalized mathematics http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/ 21 comments math
- Eff 3.0 is out, a functional language with first-class computational effects and handlers (an alternative to monads) http://math.andrej.com/eff/ 12 comments haskell
- Sometimes all functions are continuous http://math.andrej.com/2006/03/27/sometimes-all-functions-are-continuous/ 32 comments math
- Finite sets in constructive mathematics http://math.andrej.com/2009/09/07/constructive-stone-finite-sets/ 9 comments math
- On programming language design http://math.andrej.com/2009/04/11/on-programming-language-design 134 comments programming
- The Programming Languages Zoo http://math.andrej.com/2008/05/06/the-programming-languages-zoo/ 17 comments programming
- Mathematics and Computation » Representations of uncomputable and uncountable sets http://math.andrej.com/2008/02/06/representations-of-uncomputable-and-uncountable-sets/ 12 comments programming
- Seemingly Impossible Functional Programs http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/ 33 comments programming
Lambda the Ultimate
- Programming with Algebraic Effects and Handlers http://math.andrej.com/2012/03/08/programming-with-algebraic-effects-and-handlers/ 18 comments Effects , Functional
- Levy: a Toy Call-by-Push-Value Language http://math.andrej.com/2008/11/23/a-toy-call-by-push-value-language/ 4 comments Fun , Functional , Implementation , Lambda Calculus , Paradigms , Semantics , Teaching & Learning , Theory
- Eff - Language of the Future http://math.andrej.com/2010/09/27/programming-with-effects-ii-introducing-eff/ 10 comments Effects , Fun , Functional , Theory
- Synthetic Computability http://math.andrej.com/wp-content/uploads/2007/05/syncomp-mfps23.pdf 2 comments Semantics
- RZ: a tool for bringing constructive and computable mathematics closer to programming practice http://math.andrej.com/2007/01/21/rz-a-tool-for-bringing-constructive-and-computable-mathematics-closer-to-programming-practice/ 3 comments DSL , Lambda Calculus , Semantics
- Propositions as [Types] http://math.andrej.com/2004/05/04/propositions-as-types/ 5 comments Category Theory , Type Theory