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
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], 
Pure & constructive mathematics in theory and use
A Course in Universal Algebra
http://www.math.uwaterloo.ca/~snburris/htdocs/ualg.html
305 viewsUnivalence [USE GUIX, LEARN HASKELL, READ HOTT], 
Pure & constructive mathematics in theory and use
Database Implemented in Prolog is now Source-Available Free Software

https://terminusdb.com/
324 viewsGNU/Brett G., 
Pure & constructive mathematics in theory and use
Channel photo updated
Pure & constructive mathematics in theory and use
Proofs by contradiction, versus contradiction proofs

https://existentialtype.wordpress.com/2017/03/04/a-proof-by-contradiction-is-not-a-proof-that-derives-a-contradiction/
294 viewsGNU/Brett G., edited