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
Real Analysis in Reverse
http://faculty.uml.edu/jpropp/reverse.pdf
686 viewsUnivalence | quag, 
Pure & constructive mathematics in theory and use
Unfolding Finitist Arithmetic
http://math.stanford.edu/~feferman/papers/UnfoldFA.pdf
642 viewsUnivalence | quag, 
Pure & constructive mathematics in theory and use
The Unfolding of Non-Finitist Airthmetic
http://math.stanford.edu/~feferman/papers/unfolding.pdf
657 viewsUnivalence | quag, 
Pure & constructive mathematics in theory and use
Believing the Axioms
http://www.cs.umd.edu/~gasarch/BLOGPAPERS/belaxioms1.pdf
679 viewsUnivalence | quag, 
Pure & constructive mathematics in theory and use
The Strength of Mac Lane Set Theory
https://www.dpmms.cam.ac.uk/~ardm/maclane.pdf
732 viewsUnivalence | quag, 
Pure & constructive mathematics in theory and use
A Univalent Universe in Finite Order Arithmetic
https://arxiv.org/pdf/1412.6714.pdf
727 viewsUnivalence | quag, edited  
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,