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
What follows is a series of wonderful blog posts highlighting the transition of a well-established project from Python to OCaml. I hope it is useful for some of you to consider doing the same, or maybe choosing OCaml/SML or any ML for your next project!

Replacing Python: Candidates
http://roscidus.com/blog/blog/2013/06/09/choosing-a-python-replacement-for-0install/

Replacing Python: Second Round
http://roscidus.com/blog/blog/2013/06/20/replacing-python-round-2/

OCaml Binary Compatibility
http://roscidus.com/blog/blog/2013/07/07/ocaml-binary-compatibility/

Option Handling with OCaml Polymorphic Variants
http://roscidus.com/blog/blog/2013/08/31/option-handling-with-ocaml-polymorphic-variants/

Experiences with OCaml Objects
http://roscidus.com/blog/blog/2013/09/28/ocaml-objects/

OCaml Tips
http://roscidus.com/blog/blog/2013/10/13/ocaml-tips/

Asynchronous Python vs OCaml
http://roscidus.com/blog/blog/2013/11/28/asynchronous-python-vs-ocaml/

Polymorphism for Beginners
http://roscidus.com/blog/blog/2013/12/20/polymorphism-for-beginners/

OCaml: The Bugs So Far
http://roscidus.com/blog/blog/2014/01/07/ocaml-the-bugs-so-far/

OCaml: What You Gain
http://roscidus.com/blog/blog/2014/02/13/ocaml-what-you-gain/

Python to OCaml: Retrospective
http://roscidus.com/blog/blog/2014/06/06/python-to-ocaml-retrospective/
The Art of Prolog, 2e
Open Access, free PDF
https://mitpress.mit.edu/books/art-prolog-second-edition
Some HoTT Seminar whose page might be currently down depending on where you live
http://math.lsa.umich.edu/~simoncho/mwhottseminar.html
Forwarded from GNU Propaganda (Archived)
Which of these programming languages do you wish you could learn the most?
Anonymous Poll
18%
Common Lisp
11%
Scheme / Racket
8%
OCaml
2%
Mercury
3%
Prolog
9%
Scala
4%
Coq
39%
Haskell
5%
Idris
2%
Agda
Note that I'll try to do a spotlight on the language most and the language least voted for, perhaps some blog post
Haskell might be excluded because it's way too easy to find tons of material about it, Idris is more interesting
Arend, a theorem prover based on HoTT
https://arend-lang.github.io
Pure & constructive mathematics in theory and use
Same question, but based on data only gained here
Mercury and Idris, it will be. Stay tuned!
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/