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
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, 
Pure & constructive mathematics in theory and use
Taking propositions as types seriously
http://r6.ca/blog/20171008T222703Z.html
328 viewsGNU/Brett G., 
Pure & constructive mathematics in theory and use
HoTT and HITs
http://www.science4all.org/article/homotopy-type-theory/
Science4All
Homotopy Type Theory and Higher Inductive Types
In this article, we explore the possibilities allowed by higher inductive types. They enable a much more intuitive formalization of integers and new mind-blowing definitions of the (homotopical) ci…
348 viewsGNU/Brett G., 
Pure & constructive mathematics in theory and use
Kremlin
https://github.com/FStarLang/kremlin
GitHub
GitHub - FStarLang/karamel: KaRaMeL is a tool for extracting low-level F* programs to readable C code
KaRaMeL is a tool for extracting low-level F* programs to readable C code - FStarLang/karamel
304 viewsUnivalence,