-
Formalizing Correct-by-Construction in Coq
a formalization of CBC Casper using the Coq proof assistant that includes a model of the consensus protocol and proofs of safety and non-triviality protocol properties.
-
A Nonresearch Discussion
A deep conversation with my advisor
-
A flavour of type theory
a quick taste of types