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
Topology without Tears
http://www.topologywithouttears.net/topbook.pdf
http://www.topologywithouttears.net/topbook.pdf