Pure & constructive mathematics in theory and use – Telegram
Pure & constructive mathematics in theory and use
506 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
A Coq framework to support implementing, specifying, verifying, and compiling Bluespec-style hardware components with high developer productivity.
http://plv.csail.mit.edu/kami/
Mathematical Components (the book)

https://math-comp.github.io/mcb/
The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and MonadS
https://www.dpmms.cam.ac.uk/~martin/Research/Publications/2007/hp07.pdf
Database Implemented in Prolog is now Source-Available Free Software

https://terminusdb.com/
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