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
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, 
Pure & constructive mathematics in theory and use
Contravariance and Recursion
http://poleiro.info/posts/2019-08-06-contravariance-and-recursion.html
poleiro.info
Poleiro, the Coq blog - Contravariance and Recursion
A blog about the Coq proof assistant and
programming language
336 viewsGNU/Brett G., 
Pure & constructive mathematics in theory and use
My first Unikernel
http://roscidus.com/blog/blog/2014/07/28/my-first-unikernel/
Roscidus
My first unikernel - Thomas Leonard's blog
I wanted to make a simple REST service for queuing file uploads, deployable as a virtual machine. The traditional way to do this is to download a …
463 viewsGNU/Brett G., 
Pure & constructive mathematics in theory and use
Typed Combinators
http://chriswarbo.net/blog/2012-12-01-typed_combinators.html
389 viewsGNU/Brett G., 
Pure & constructive mathematics in theory and use
Simplicial Sets are Algorithms
http://therisingsea.org/notes/MScThesisWillTroiani.pdf
386 viewsUnivalence, edited  
Pure & constructive mathematics in theory and use
Equations reloaded: high-level dependently typed functional programming and proving in Coq

https://dl.acm.org/citation.cfm?id=3341690
438 viewsGNU/Brett G.,