Pure & constructive mathematics in theory and use – Telegram
Pure & constructive mathematics in theory and use
507 subscribers
1 photo
13 files
444 links
Just resources about fundamental mathematics, type theory, their use in programming mostly.
Contact: @megamanisepic
Becoming an admin isn't difficult as long as you have a slight idea of the topic and preserve the style.
Download Telegram
Reflections on Standard ML

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
Backprop as Functor: A compositional perspective on supervised learning

https://arxiv.org/pdf/1711.10455.pdf
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!
The Type Theory Podcast
http://typetheorypodcast.com/
Kerodon - an online resource for homotopy-coherent mathematics
https://kerodon.net/kerodon.pdf
WIP book, requires basic knowledge of topology.
[Thanks to H]
CakeML: A Verified Implementation of Standard ML

https://cakeml.org/
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)