Pure & constructive mathematics in theory and use – Telegram
Pure & constructive mathematics in theory and use
@typetheoryinprogramming
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
About
Blog
Apps
Platform
Join
Pure & constructive mathematics in theory and use
506 subscribers
Pure & constructive mathematics in theory and use
The Art of Prolog, 2e
Open Access, free PDF
https://mitpress.mit.edu/books/art-prolog-second-edition
422 viewsGNU/Brett G., edited  
Pure & constructive mathematics in theory and use
Some HoTT Seminar whose page might be currently down depending on where you live
http://math.lsa.umich.edu/~simoncho/mwhottseminar.html
286 viewsUnivalence [USE GUIX, LEARN HASKELL, READ HOTT], edited  
Pure & constructive mathematics in theory and use
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
330 voters30 viewsGNU/Brett G., 
Pure & constructive mathematics in theory and use
Same question, but based on data only gained here
Anonymous Poll
15%
Common Lisp
7%
Scheme / Racket
9%
(OCa)ML
3%
Mercury
5%
Prolog
2%
Scala
6%
Coq
32%
Haskell
14%
Idris
6%
Agda
98 voters356 viewsUnivalence [USE GUIX, LEARN HASKELL, READ HOTT], 
Pure & constructive mathematics in theory and use
Note that I'll try to do a spotlight on the language most and the language least voted for, perhaps some blog post
387 viewsUnivalence [USE GUIX, LEARN HASKELL, READ HOTT], 
Pure & constructive mathematics in theory and use
Haskell might be excluded because it's way too easy to find tons of material about it, Idris is more interesting
390 viewsUnivalence [USE GUIX, LEARN HASKELL, READ HOTT], 
Pure & constructive mathematics in theory and use
Arend, a theorem prover based on HoTT
https://arend-lang.github.io
468 viewsUnivalence [USE GUIX, LEARN HASKELL, READ HOTT], 
Pure & constructive mathematics in theory and use
ETCS
https://ncatlab.org/nlab/show/ETCS
525 viewsGNU/Brett G., 
Pure & constructive mathematics in theory and use
pi-base, a database of topological spaces
https://topology.jdabbs.com/
π-Base
A community database of topological theorems and spaces, with powerful search and automated proof deduction.
502 viewsUnivalence [USE GUIX, LEARN HASKELL, READ HOTT], 
Pure & constructive mathematics in theory and use
Pure & constructive mathematics in theory and use
Same question, but based on data only gained here
Mercury and Idris, it will be. Stay tuned!
453 viewsUnivalence [USE GUIX, LEARN HASKELL, READ HOTT], 
Pure & constructive mathematics in theory and use
What does a humped critter have to teach us?
https://markkarpov.com/post/what-does-a-humped-critter-have-to-teach-us.html
Markkarpov
What does a humped critter have to teach us?
430 viewsGNU/Brett G. (Away), 
Pure & constructive mathematics in theory and use
The Future of OCaml
https://ocamlverse.github.io/content/future_ocaml.html
OCamlverse
Future of OCaml
Documenting everything about OCaml
481 viewsUnivalence [USE GUIX, LEARN HASKELL, READ HOTT], 
Pure & constructive mathematics in theory and use
A Coq framework to support implementing, specifying, verifying, and compiling Bluespec-style hardware components with high developer productivity.
http://plv.csail.mit.edu/kami/
336 viewsGNU/Brett G., 
Pure & constructive mathematics in theory and use
Mathematical Components (the book)

https://math-comp.github.io/mcb/
314 viewsGNU/ Tarski (rewritten in Rust), edited  
Pure & constructive mathematics in theory and use
Agda Cheatsheet
https://github.com/alhassy/AgdaCheatSheet
GitHub
GitHub - alhassy/AgdaCheatSheet: Basics of the dependently-typed functional language Agda ^_^
Basics of the dependently-typed functional language Agda ^_^ - alhassy/AgdaCheatSheet
322 viewsGNU/Brett G., 
Pure & constructive mathematics in theory and use
Parallel & Distributed Operating Systems Group
https://pdos.csail.mit.edu/
pdos.csail.mit.edu
MIT CSAIL Parallel and Distributed Operating Systems Group
MIT CSAIL Parallel and Distributed Operating Systems homepage
308 viewsGNU/Brett G., 
Pure & constructive mathematics in theory and use
You are already smart enough to write Haskell
https://williamyaoh.com/posts/2019-10-05-you-are-already-smart-enough.html
373 viewsUnivalence [USE GUIX, LEARN HASKELL, READ HOTT], edited  
Pure & constructive mathematics in theory and use
BigraphER
http://www.dcs.gla.ac.uk/~michele/bigrapher.html
322 viewsGNU/Brett G., 
Pure & constructive mathematics in theory and use
PRISM
http://www.prismmodelchecker.org/
351 viewsGNU/Brett G., 
Pure & constructive mathematics in theory and use
The History of Standard ML: Ideas, Principles, Culture
https://www.youtube.com/watch?v=NVEgyJCTee4
YouTube
01 The History of Standard ML: Ideas, Principles, Culture
Enjoy the videos and music you love, upload original content, and share it all with friends, family, and the world on YouTube.
366 viewsGNU/Brett G., 
Pure & constructive mathematics in theory and use
The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and MonadS
https://www.dpmms.cam.ac.uk/~martin/Research/Publications/2007/hp07.pdf
766 viewsUnivalence [USE GUIX, LEARN HASKELL, READ HOTT],