Pure & constructive mathematics in theory and use – Telegram
Pure & constructive mathematics in theory and use
@typetheoryinprogramming
513 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
513 subscribers
Pure & constructive mathematics in theory and use
A synthetic theory of infinity-categories in homotopy type theory
http://www.math.jhu.edu/~eriehl/octoberfest.pdf
263 views(A = B) ~ (A ~ B), 
Pure & constructive mathematics in theory and use
No noscript #1
http://okmij.org/ftp/
A very functional blog
okmij.org
This FTP site
Main index of okmij.org
282 views(A = B) ~ (A ~ B), 
Pure & constructive mathematics in theory and use
Applied Category Theory conference
https://www.youtube.com/user/wires0/live
Note that this is a livestream.
YouTube
Jelle Herold
275 views(A = B) ~ (A ~ B), 
Pure & constructive mathematics in theory and use
... and its programme, thanks to Daniele.
269 views(A = B) ~ (A ~ B), 
Pure & constructive mathematics in theory and use
Forwarded from Daniele
ACT 2019 programme.pdf
304.2 KB
284 views(A = B) ~ (A ~ B), 
Pure & constructive mathematics in theory and use
HoTT-2019
https://vimeo.com/channels/1457250
Video lectures on HoTT by Andrej Bauer!
Vimeo
2019-HoTT Introduction to homotopy type theory
Video recordings of doctoral lectures on homotopy type theory, Spring 2019, Faculty of Mathematics and Physics, University of Ljubljana. See https://github.com/andrejbauer/homotopy-type-theory-course…
324 views(A = B) ~ (A ~ B), 
Pure & constructive mathematics in theory and use
Guix: A most advanced operating system
https://ambrevar.xyz/guix-advance/
The superior, purely functional package manager.
328 views(A = B) ~ (A ~ B), 
Pure & constructive mathematics in theory and use
NixOS
https://nixos.org/nixos/
As well purely functional, with its own advantages and disadvantages compared to Guix.
301 views(A = B) ~ (A ~ B), 
Pure & constructive mathematics in theory and use
Guix
http://guix.gnu.org
guix.gnu.org
GNU Guix transactional package manager and distribution — GNU Guix
Guix is a distribution of the GNU operating system.
Guix is technology that respects the freedom of computer users.
You are free to run the system for any purpose, study how it
works, improve it, and share it with the whole world.
351 views(A = B) ~ (A ~ B), 
Pure & constructive mathematics in theory and use
Dedukti
https://deducteam.github.io/index.html
Dedukti is a logical framework based on the λΠ-calculus modulo in which many theories and logics can be expressed.
318 views(A = B) ~ (A ~ B), edited  
Pure & constructive mathematics in theory and use
The Lean Theorem Prover
https://homotopytypetheory.org/2015/12/02/the-proof-assistant-lean/
Homotopy Type Theory
The Lean Theorem Prover
Lean is a new player in the field of proof assistants for Homotopy Type Theory. It is being developed by Leonardo de Moura working at Microsoft Research, and it is still under active development fo…
375 views(A = B) ~ (A ~ B), edited  
Pure & constructive mathematics in theory and use
Thanks for 100 members!
372 views(A = B) ~ (A ~ B), 
Pure & constructive mathematics in theory and use
As I got a shoutout by @GNUPropaganda, I'd want everyone interested in free software to join there, as well @GNUGroup (you need an invite for that one though). Also, to engage in in-depth discussion about type theory and formal verification, join @deepspec!
402 views(A = B) ~ (A ~ B), 
Pure & constructive mathematics in theory and use
poly
https://github.com/Bodigrim/poly
Univariate polynomials in Haskell.
GitHub
Bodigrim/poly
Fast polynomial arithmetic in Haskell. Contribute to Bodigrim/poly development by creating an account on GitHub.
456 views(A = B) ~ (A ~ B), 
Pure & constructive mathematics in theory and use
A categorical construction for the computational definition of vector spaces
https://arxiv.org/abs/1905.01305
arXiv.org
A categorical construction for the computational definition of...
Lambda-S is an extension to first-order lambda calculus unifying two
approaches of non-cloning in quantum lambda-calculi. One is to forbid
duplication of variables, while the other is to consider...
337 views(A = B) ~ (A ~ B), 
Pure & constructive mathematics in theory and use
Abstracting Extensible Data Types
http://ittc.ku.edu/~garrett/pubs/morris-popl2019-rows.pdf?
339 views(A = B) ~ (A ~ B), 
Pure & constructive mathematics in theory and use
Types as Graphs: Continuations in Type Logical Grammar
http://www.nyu.edu/projects/barker/barker-shan-types-as-graphs.pdf
393 views(A = B) ~ (A ~ B), 
Pure & constructive mathematics in theory and use
Proof mining
https://pdfs.semanticscholar.org/561c/72b96b33f68f4b2936524a465c578b5fca74.pdfhttps://pdfs.semanticscholar.org/561c/72b96b33f68f4b2936524a465c578b5fca74.pdf
458 views(A = B) ~ (A ~ B), 
Pure & constructive mathematics in theory and use
A Principled Approach to Operating System Construction in Haskell
http://ogi.altocumulus.org/~hallgren/ICFP2005/house.pdf
399 views(A = B) ~ (A ~ B), edited  
Pure & constructive mathematics in theory and use
Omega
https://code.google.com/archive/p/omega/
406 views(A = B) ~ (A ~ B), 
Pure & constructive mathematics in theory and use
Programs and Proofs
https://ilyasergey.net/pnp/
425 views(A = B) ~ (A ~ B),