Pure & constructive mathematics in theory and use – Telegram
Pure & constructive mathematics in theory and use
@typetheoryinprogramming
514 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
514 subscribers
Pure & constructive mathematics in theory and use
Andrea Vezzosi - Indexed Families in Cubical Agda.pdf
74 KB
Indexed Families' computation in Cubical Agda
656 viewsTeslArend Zhang, 
Pure & constructive mathematics in theory and use
An Introduction to Proof Theory
http://www.math.ucsd.edu/~sbuss/ResearchWeb/handbookI/ChapterI.pdf
676 viewsUnivalence | quag, 
Pure & constructive mathematics in theory and use
The Art of Ordinal Analysis
https://web.archive.org/web/20091222002129/http://www.icm2006.org/proceedings/Vol_II/contents/ICM_Vol_2_03.pdf
695 viewsUnivalence | quag, 
Pure & constructive mathematics in theory and use
First-Order Theorem Proving and Vampire
http://www.vprover.org/cav2013.pdf
606 viewsUnivalence | quag, edited  
Pure & constructive mathematics in theory and use
Proof Theory and Computational Analysis
https://www.researchgate.net/publication/222487825_Proof_Theory_and_Computational_Analysis/fulltext/0fa4ed830cf22f7ae5efaad8/Proof-Theory-and-Computational-Analysis.pdf
647 viewsUnivalence | quag, edited  
Pure & constructive mathematics in theory and use
Transfinite Ordinals and their Notations
http://www.cs.fsu.edu/~levitz/ords.ps
545 viewsUnivalence | quag, 
Pure & constructive mathematics in theory and use
An Introduction to Set Theory
https://www.math.toronto.edu/weiss/set_theory.pdf
675 viewsUnivalence | quag, 
Pure & constructive mathematics in theory and use
Introduction to Ordinal Analysis
https://www.uni-goettingen.de/de/document/download/1bb43144c8c4bb68805337a25d8d1db9.pdf/pohlers_handout_3.pdf
559 viewsUnivalence | quag, 
Pure & constructive mathematics in theory and use
First- and Second-Order Models of Recursive Arithmetics
https://arxiv.org/pdf/1705.05459.pdf
574 viewsUnivalence | quag, 
Pure & constructive mathematics in theory and use
Algebraic Topology
https://pi.math.cornell.edu/~hatcher/AT/AT.pdf
657 viewsUnivalence | quag, 
Pure & constructive mathematics in theory and use
Non-commutative Logic I: the Multiplicative Fragment
https://static.aminer.org/pdf/PDF/000/753/432/non_commutative_logic_i_the_multiplicative_fragment.pdf
703 viewsUnivalence | quag, 
Pure & constructive mathematics in theory and use
A Formally Verified Abstract Account of Gödel's Incompleteness Theorems
https://www21.in.tum.de/~traytel/papers/cade19-incompleteness/incompleteness.pdf
770 viewsUnivalence | quag, edited  
Pure & constructive mathematics in theory and use
4_5831262430465884843.pdf
218.5 KB
Corecursion and coinduction: how they relate to recursion and induction
833 viewsParra, edited  
Pure & constructive mathematics in theory and use
Three Equivalent Ordinal Notation Systems in Cubical Agda
https://arxiv.org/pdf/1904.10759.pdf
698 viewsUnivalence | quag, 
Pure & constructive mathematics in theory and use
Ordinals and Interactive Programs
https://pdfs.semanticscholar.org/89c9/a2bca07752f9ed631c304bad8c34c2b163a2.pdf
780 viewsUnivalence | quag, edited  
Pure & constructive mathematics in theory and use
4_5862880936021983758.pdf
1 MB
Fundamental Theorems in Mathematics (2019)
855 viewsParra, edited  
Pure & constructive mathematics in theory and use
A tutorial implementation of a dependently typed Lambda Calculus
https://www.andres-loeh.de/LambdaPi/LambdaPi.pdf
[Thanks to Elias]
735 viewsUnivalence | quag, 
Pure & constructive mathematics in theory and use
Self-Verifying Axiom Systems, the Incompleteness Theorem and Related Reflection Principles
https://www.cs.albany.edu/~dew/m/jsl1.pdf
689 viewsUnivalence | quag, 
Pure & constructive mathematics in theory and use
Summary of Truth about Types
https://rakhim.org/summary-of-truth-about-types-a-talk-by-bartosz-milewski/
672 viewsParra, 
Pure & constructive mathematics in theory and use
Categorical Semantics of Digital Circuits
https://www.cs.bham.ac.uk/~drg/papers/fmcad16.pdf
[Thanks to Victor]
706 viewsUnivalence | quag, 
Pure & constructive mathematics in theory and use
Semantics of higher inductive types
https://arxiv.org/abs/1705.07088
708 viewsTeslArend Zhang, edited