Search

• https://martin.kleppmann.com/2022/10/12/verifying-distributed-systems-isabelle.html
• https://conferences.computer.org/eurosp/pdfs/EuroSPW2020-7k9FlVRX4z43j4uE2SeXU0/859700a634/859700a634.pdf
• https://www.youtube.com/watch?v=Dp-mQ3HxgDE
• https://dl.acm.org/doi/abs/10.1145/3571258

Imp.v

Inductive propositions confused me so much I decided to make a note for it.

Install Ocaml

Non-automatic

In simple terms, $\lambda$-calculus is a way to specify function applications without actually defining their names. Normally in programming, we can define a function like so:

let f(x) = x * x + 1 in B