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
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, 
Pure & constructive mathematics in theory and use
Categorical Logic by Andrew M. Pitts https://www.cl.cam.ac.uk/~amp12/papers/catl/catl.pdf
2.22K viewsTesla Zhang, 
Pure & constructive mathematics in theory and use
Categories with Families: Unityped, Simply Typed, and Dependently Typed https://arxiv.org/abs/1904.00827
2.3K viewsTesla Zhang, 
Pure & constructive mathematics in theory and use
A Minimalistic Verified Bootstrapped Compiler
https://popl21.sigplan.org/details/CPP-2021/6/A-Minimalistic-Verified-Bootstrapped-Compiler-Proof-Pearl-
popl21.sigplan.org
A Minimalistic Verified Bootstrapped Compiler (Proof Pearl) (CPP 2021 - Certified Programs and Proofs) - POPL 2021
Certified Programs and Proofs (CPP) is an international conference on practical and theoretical topics in all areas that consider formal verification and certification as an essential paradigm for their work. CPP spans areas of computer science, mathematics…
2.49K viewsParra, 
Pure & constructive mathematics in theory and use
Cubical Agda paper v2 with transpX discussed
https://staff.math.su.se/anders.mortberg/papers/cubicalagda2.pdf
2.59K viewsTesla Zhang, 
Pure & constructive mathematics in theory and use
RefinedC

Automating the Foundational Verification of C Code with Refined Ownership Types

https://plv.mpi-sws.org/refinedc/
2.62K viewsParra, 
Pure & constructive mathematics in theory and use
Choosing is Losing:
How to combine the benefits of shallow and deep embeddings through reflection in dependently-typed host languages

https://arxiv.org/abs/2105.10819
3.01K viewsParra, 
Pure & constructive mathematics in theory and use
Synthesis of Heap-Manipulating Programs from Separation Logic
https://gopiandcode.uk/logs/log-certified-synthesis.html
gopiandcode.uk
Gopiandcode > logs > Goodbye C developers: The future of programming with certified program synthesis
3K viewsParra,