Generic Theorem Proving Using Hol2p: A Category Theory Inspired Approach
https://core.ac.uk/download/pdf/132207455.pdf
https://core.ac.uk/download/pdf/132207455.pdf
[Proposal] The Formal Methods in GNU Guix working group
https://paste.sr.ht/~brettgilio/111ac260827a2a77e0f836bc5a1c4f8188eff1ca
https://paste.sr.ht/~brettgilio/111ac260827a2a77e0f836bc5a1c4f8188eff1ca
Computational interpretations of linear logic
https://core.ac.uk/download/pdf/81933277.pdf
https://core.ac.uk/download/pdf/81933277.pdf
I Got Plenty o' Nuttin'
https://personal.cis.strath.ac.uk/conor.mcbride/PlentyO-CR.pdf
Combining linear and dependent types.
[Thanks to ptrcmd]
https://personal.cis.strath.ac.uk/conor.mcbride/PlentyO-CR.pdf
Combining linear and dependent types.
[Thanks to ptrcmd]
Inductive Reasoning about Effectful Data Types
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.92.4123&rep=rep1&type=pdf
[Thanks to swarnim]
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.92.4123&rep=rep1&type=pdf
[Thanks to swarnim]
An Outline of Algebraic Set Theory
http://caae.phil.cmu.edu/projects/ast/Papers/awodey_outline.pdf
http://caae.phil.cmu.edu/projects/ast/Papers/awodey_outline.pdf
Channel name was changed to «Pure & constructive mathematics in theory and use»
Algebraic Topology (Lecture Notes)
https://www.mit.edu/~sanathd/main.pdf
https://www.mit.edu/~sanathd/main.pdf
An Introduction to Higher Categorical Algebra
https://arxiv.org/abs/1907.02904
https://arxiv.org/abs/1907.02904
Higher Topos Theory
https://arxiv.org/abs/math/0608040v4
https://arxiv.org/abs/math/0608040v4
Higher Algebra
https://arxiv.org/abs/math/0608040v4
https://arxiv.org/abs/math/0608040v4
Towards Observational Type Theory
http://strictlypositive.org/ott.pdf
http://strictlypositive.org/ott.pdf
Topology without Tears
http://www.topologywithouttears.net/topbook.pdf
http://www.topologywithouttears.net/topbook.pdf
Exhaustible Sets in Higher-type Computation
https://www.researchgate.net/publication/220346819_Exhaustible_Sets_in_Higher-type_Computation
(free to download, no request required)
https://www.researchgate.net/publication/220346819_Exhaustible_Sets_in_Higher-type_Computation
(free to download, no request required)
ResearchGate
(PDF) Exhaustible Sets in Higher-type Computation.
PDF | We say that a set is exhaustible if it admits algorithmic universal quantification for continuous predicates in finite time, and searchable if... | Find, read and cite all the research you need on ResearchGate
Infinite Sets that admit fast exhaustive search
https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.127.3062
https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.127.3062
citeseerx.ist.psu.edu
CiteSeerX — Infinite sets that admit fast exhaustive search
CiteSeerX - Document Details (Isaac Councill, Lee Giles, Pradeep Teregowda): Abstract. Perhaps surprisingly, there are infinite sets that admit mechanical exhaustive search in finite time. An old example is the Cantor space of infinite sequences of binary…
The Strict ω-Groupoid Interpretation of Type Theory
https://mawarren.net/papers/crmp1295.pdf
https://mawarren.net/papers/crmp1295.pdf
Globular
http://globular.science/
http://globular.science/