This is a condensed summary of “A Tutorial on (Co)Algebras and (Co)Induction” by Jacobs and Rutten. Note that this is for personal recall and hence unstructured.

Traditional induction on nat is defined as the following:

A trace of a program execution is the sequence of transitions of the program state:

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

basics

(referenced from logsem iris tutorial)

\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