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
Logic, Languages, Compilation, and Verification
http://www.cs.uoregon.edu/research/summerschool/summer12/curriculum.html
http://www.cs.uoregon.edu/research/summerschool/summer12/curriculum.html
Seemingly impossible functional programs
http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/
http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/
Category Theory with Bartosz Milewski: podcast
https://corecursive.com/035-bartosz-milewski-category-theory/
https://corecursive.com/035-bartosz-milewski-category-theory/
CoRecursive Podcast
Category Theory - CoRecursive Podcast
Today Adam talks to Bartosz Milewski. He is the author of a popular blog series, lecture series, and now book on Category Theory for programmers.The world of functional programming is rife with terminology imported from abstract algebra and Category Theory.…
The Type Theory Podcast
http://typetheorypodcast.com/
http://typetheorypodcast.com/
Homotopy Patch Theory
http://dlicata.web.wesleyan.edu/pubs/amlh14patch/amlh14patch.pdf
http://dlicata.web.wesleyan.edu/pubs/amlh14patch/amlh14patch.pdf
Kerodon - an online resource for homotopy-coherent mathematics
https://kerodon.net/kerodon.pdf
WIP book, requires basic knowledge of topology.
[Thanks to H]
https://kerodon.net/kerodon.pdf
WIP book, requires basic knowledge of topology.
[Thanks to H]
Forwarded from Cab
Also, a little disclamer. We have small meetings each Wednesday evening, chatting about category theory, Coq, ssreflect, HoTT, FP in general, NixOS — and all that good stuff. We are gathering in Kocherga (Moscow).
If you want to participate — PM me) (usually comes from 4 to 6 people)
If you want to participate — PM me) (usually comes from 4 to 6 people)
The Five Stages of Accepting Constructive Mathematics: Andrej Bauer
https://www.youtube.com/watch?v=21qPOReu4FI
https://www.youtube.com/watch?v=21qPOReu4FI
YouTube
Five Stages of Accepting Constructive Mathematics - Andrej Bauer
Andrej Bauer
University of Ljubljana, Slovenia; Member, School of Mathematics
March 18, 2013
Discussions about constructive mathematics are usually derailed by philosophical opinions and meta-mathematics. But how does it actually feel to do constructive mathematics?…
University of Ljubljana, Slovenia; Member, School of Mathematics
March 18, 2013
Discussions about constructive mathematics are usually derailed by philosophical opinions and meta-mathematics. But how does it actually feel to do constructive mathematics?…