Separation Logic is an extension of Hoare Logic to reason about local regions of a program state.

WIP

\mathcal

After installing code-server through the installation script, systemctl can fail to start code-server.service:

Consequence Rule

Search

• Abstract Interpretation in Coq
• Skeletal Semantics and their Interpretations
• https://martin.kleppmann.com/2022/10/12/verifying-distributed-systems-isabelle.html
• Program Obfuscation Coq
• Compcert Memory Model
• Incorrectness logic
• Interaction trees

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