3 ms·
Ha, I actually wrote a paper pushing on this "kernel" pun between OSs and proof-checkers [1], designing a HOL kernel structured like an OS kernel. [1]: https:/
by dmulligan 2mo ago
Ha, I actually wrote a paper pushing on this "kernel" pun between OSs and proof-checkers [1], designing a HOL kernel structured like an OS kernel.
[1]: https://drops.dagstuhl.de/storage/00lipics/lipics-vol269-types2022/LIPIcs.TYPES.2022.1/LIPIcs.TYPES.2022.1.pdf https://drops.dagstuhl.de/storage/00lipics/lipics-vol269-typ...