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
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), 
Pure & constructive mathematics in theory and use
The Coq Effective Algebra Library
https://github.com/CoqEAL/CoqEAL
GitHub
CoqEAL/CoqEAL
CoqEAL -- The Coq Effective Algebra Library. Contribute to CoqEAL/CoqEAL development by creating an account on GitHub.
409 views(A = B) ~ (A ~ B), 
Pure & constructive mathematics in theory and use
Towards Higher Universal Algebra in Type Theory
https://ncatlab.org/nlab/files/Finster-2018-HoTTEST-compact.pdf
370 views(A = B) ~ (A ~ B), 
Pure & constructive mathematics in theory and use
Groupoid Infinity (?)
https://groupoid.space/
groupoid.space
GROUPOЇD
413 views(A = B) ~ (A ~ B), 
Pure & constructive mathematics in theory and use
Parameterized Compilability
https://ijcai.org/Proceedings/05/Papers/0644.pdf
[thanks to no_identd]
399 views(A = B) ~ (A ~ B), 
Pure & constructive mathematics in theory and use
Follow-up: https://www.ac.tuwien.ac.at/research/parameterized-compilation/
427 views(A = B) ~ (A ~ B), 
Pure & constructive mathematics in theory and use
Some algebraic structures
https://en.wikipedia.org/wiki/User:Rschwieb/Cold_storage
Wikipedia
User:Rschwieb/Cold storage
The following two structures form a bridge connecting magmas and lattices:
423 views(A = B) ~ (A ~ B), 
Pure & constructive mathematics in theory and use
The Granule project
https://granule-project.github.io/
Modal, dependent types in practical use, so it seems.
555 viewsUnivalence, 
Pure & constructive mathematics in theory and use
Out of the tarpit
http://curtclifton.net/papers/MoseleyMarks06a.pdf
349 viewsUnivalence,