You are already smart enough to write Haskell
https://williamyaoh.com/posts/2019-10-05-you-are-already-smart-enough.html
https://williamyaoh.com/posts/2019-10-05-you-are-already-smart-enough.html
The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and MonadS
https://www.dpmms.cam.ac.uk/~martin/Research/Publications/2007/hp07.pdf
https://www.dpmms.cam.ac.uk/~martin/Research/Publications/2007/hp07.pdf
A Course in Universal Algebra
http://www.math.uwaterloo.ca/~snburris/htdocs/ualg.html
http://www.math.uwaterloo.ca/~snburris/htdocs/ualg.html
Proofs by contradiction, versus contradiction proofs
https://existentialtype.wordpress.com/2017/03/04/a-proof-by-contradiction-is-not-a-proof-that-derives-a-contradiction/
https://existentialtype.wordpress.com/2017/03/04/a-proof-by-contradiction-is-not-a-proof-that-derives-a-contradiction/
Reflections on Standard ML
http://sml-family.org/papers/MacQueen-reflections.pdf
Standard ML is one of a number of new programming languages developed in the 1980s that are seen as suitable vehicles for serious systems and applications programming. It offers an excellent ratio of expressiveness to language complexity, and provides competitive efficiency. Because of its type and module system, Standard ML manages to combine safety, security, and robustness with much of the flexibility of dynamically typed languages like Lisp. It is also has the most well-developed scientific foundation of any major language. Here I review the strengths and weaknesses of Standard ML and describe some of what we have learned through the design, implementation, and use of the language.
http://sml-family.org/papers/MacQueen-reflections.pdf
Resource Aware ML
http://raml.co/index.html
http://raml.co/index.html
raml.co
Resource Aware ML
Coq 8.10.0 released
https://coq.inria.fr/news/coq-8-10-0-is-out.html
https://coq.inria.fr/news/coq-8-10-0-is-out.html
Backprop as Functor: A compositional perspective on supervised learning
https://arxiv.org/pdf/1711.10455.pdf
https://arxiv.org/pdf/1711.10455.pdf
Algebraic Graphs in Functional Programming
https://github.com/snowleopard/alga-paper
[Thanks to swarnim]
https://github.com/snowleopard/alga-paper
[Thanks to swarnim]
GitHub
GitHub - snowleopard/alga-paper: A minimalistic, elegant and powerful approach to working with graphs in a functional programming…
A minimalistic, elegant and powerful approach to working with graphs in a functional programming language - snowleopard/alga-paper
Episode 5: Bob Constable on CTT and Nuprl
http://typetheorypodcast.com/2015/08/episode-5-bob-constable-on-ctt-and-nuprl/
http://typetheorypodcast.com/2015/08/episode-5-bob-constable-on-ctt-and-nuprl/
The Type Theory Podcast
Episode 5: Bob Constable on CTT and Nuprl
Forwarded from Brett G.
Interested in enhancing type theory, theoretical mathematics, and functional programming for industry-grade software?
Symode is a company developed on the principle that elegant design and logical rigor must coexist in the intersection of mathematics and programming. Symode is looking for contributors to our mutual project to enhance software with safety and fault-tolerant design.
Stay tuned for more information!
Symode is a company developed on the principle that elegant design and logical rigor must coexist in the intersection of mathematics and programming. Symode is looking for contributors to our mutual project to enhance software with safety and fault-tolerant design.
Stay tuned for more information!
EventML: A functional programmming language with high level combinators that works with the Nuprl theorem prover
http://www.nuprl.org/software/
http://www.nuprl.org/software/
www.nuprl.org
EventML
implementing computational mathematics and providing logic-based tools that help automate programming
