Also, please let me know if you have any content, or would like to be an admin. The more information, the better!
On the Effects of Static Typing in Detecting Public Bugs
http://ttendency.cs.ucl.ac.uk/projects/type_study/
http://ttendency.cs.ucl.ac.uk/projects/type_study/
Checking Dependent Types with Normalization by Evaluation: A Tutorial
http://davidchristiansen.dk/tutorials/nbe/
http://davidchristiansen.dk/tutorials/nbe/
Forwarded from uni
http://davidchristiansen.dk/tutorials/implementing-types-hs.pdf
The same, but in Haskell
The same, but in Haskell
A Tutorial on Using Dafny to Construct Verified Software
https://arxiv.org/pdf/1701.04481.pdf
[Thanks to ptrcmd]
https://arxiv.org/pdf/1701.04481.pdf
[Thanks to ptrcmd]
Hurd, seL4, thoughts
https://nalaginrut.com/archives/2019/12/11/hurd%2c%20sel4%2c%20thoughts
https://nalaginrut.com/archives/2019/12/11/hurd%2c%20sel4%2c%20thoughts
Boeing and Deaths due to Software Bugs | Marko Dimjašević
https://dimjasevic.net/marko/2019/04/08/boeing-and-deaths-due-to-software-bugs/index.html
https://dimjasevic.net/marko/2019/04/08/boeing-and-deaths-due-to-software-bugs/index.html
Interim
https://github.com/eudoxia0/interim
Low-level lisp with compile-time memory management
[Thanks to Would]
https://github.com/eudoxia0/interim
Low-level lisp with compile-time memory management
[Thanks to Would]
GitHub
GitHub - eudoxia0/interim: Low-level Lisp with compile-time memory management
Low-level Lisp with compile-time memory management - eudoxia0/interim
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