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
Rectangular Axioms, perfect set properties and decomposition
http://www.users.miamioh.edu/larsonpb/goedel.pdf
762 viewsUnivalence | quag, 
Pure & constructive mathematics in theory and use
Concept Calculus
https://cpb-us-w2.wpmucdn.com/u.osu.edu/dist/1/1952/files/2014/01/ConcCalcMIT110409-2ddqhmp.pdf
799 viewsUnivalence | quag, 
Pure & constructive mathematics in theory and use
Number theory and elementary arithmetic
http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=0F5B8AAA8EBE01A962B6B0DAA8A7A873?doi=10.1.1.105.6509&rep=rep1&type=pdf
827 viewsUnivalence | quag, 
Pure & constructive mathematics in theory and use
Cardinal Arithmetic in the style of Baron von Münchhausen
https://dspace.library.uu.nl/bitstream/handle/1874/33720/preprint272.pdf?sequence=1&isAllowed=y
952 viewsUnivalence | quag, 
Pure & constructive mathematics in theory and use
Nonstandard Models of Arithmetic
https://diagonalargument.com/mathnotes/nonstandard-models-of-arithmetic-the-series/
Diagonal Argument
Nonstandard Models of Arithmetic: The Series
John Baez and I have been conducting a conversation about nonstandard models of Peano arithmetic (PA). This page serves as an annotated table of contents, bibliography, and general repository for s…
1.15K viewsUnivalence | quag, edited  
Pure & constructive mathematics in theory and use
What is effective transfinite recursion in reverse mathematics?
https://arxiv.org/pdf/2006.08953.pdf
1.23K viewsUnivalence | quag, 
Pure & constructive mathematics in theory and use
Representing contractive functions on streams
http://www.cs.nott.ac.uk/~pszgmh/contractive.pdf
1.22K viewsUnivalence | quag, 
Pure & constructive mathematics in theory and use
Type-Based Methods for Termination and Productivity in Coq
https://coq.inria.fr/files/coq5_submission_5.pdf
1.14K viewsTesla Zhang, edited  
Pure & constructive mathematics in theory and use
Integrating Dependent and Linear Types
https://www.cl.cam.ac.uk/~nk480/dlnl-paper.pdf
1.27K viewsUnivalence | quag, 
Pure & constructive mathematics in theory and use
A survey of compatibility logic
https://arxiv.org/abs/1612.04513
http://www.csc.villanova.edu/~japaridz/CL/
1.3K viewsUnivalence, edited  
Pure & constructive mathematics in theory and use
Strict Set (which Agda calls SSet) comes from 2-level type theory, see https://arxiv.org/pdf/1705.03307.pdf and https://arxiv.org/pdf/1604.03799.pdf)
1.3K viewsTesla Zhang, 
Pure & constructive mathematics in theory and use
https://arxiv.org/abs/2001.10490
Lean's approach to hygiene macros
1.4K viewsTesla Zhang, 
Pure & constructive mathematics in theory and use
A classical sequent calculus with dependent types
https://hal.archives-ouvertes.fr/hal-01744359/document
1.39K viewsUnivalence, 
Pure & constructive mathematics in theory and use
Introduction to Categories and Categorical Logic
https://arxiv.org/abs/1102.1313
1.5K viewsUnivalence, 
Pure & constructive mathematics in theory and use
Introduction to Homotopy Type Theory
https://github.com/EgbertRijke/HoTT-Intro
GitHub
GitHub - EgbertRijke/HoTT-Intro: An introductory course to Homotopy Type Theory
An introductory course to Homotopy Type Theory. Contribute to EgbertRijke/HoTT-Intro development by creating an account on GitHub.
2.3K viewsParra, 
Pure & constructive mathematics in theory and use
The Stacks Project
https://stacks.math.columbia.edu/browse
stacks.math.columbia.edu
Table of contents—The Stacks project
an open source textbook and reference work on algebraic geometry
2.41K viewsUnivalence, 
Pure & constructive mathematics in theory and use
Forwarded from Tony Xu
While we're still at it, I'd like to announce my project to formalize the Stacks project in Arend
2.24K viewsTesla Zhang, 
Pure & constructive mathematics in theory and use
Forwarded from Tony Xu
https://github.com/tonyxty/hStacks
GitHub
GitHub - tonyxty/hStacks: Stacks project, from a homotopy type theory point-of-view (hPOV)
Stacks project, from a homotopy type theory point-of-view (hPOV) - tonyxty/hStacks
1.55K viewsTesla Zhang, 
Pure & constructive mathematics in theory and use
75 Problems for Testing Automated Theorem Provers
http://www.sfu.ca/~jeffpell/papers/75ATPproblems86.pdf
1.89K viewsUnivalence, 
Pure & constructive mathematics in theory and use
Denotational Design with Typeclass Morphisms
http://conal.net/papers/type-class-morphisms/type-class-morphisms-long.pdf
1.97K viewsUnivalence, 
Pure & constructive mathematics in theory and use
Fast and Loose Reasoning is Morally Correct
https://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loose.pdf
2.26K viewsParra,