HOL

Axioms

Encoding forall ``\x P(x) = \x true` is saying that the predictae p is always true.

HOL

• cakeml a verified implementation of an ML in HOL4
• holpy https://arxiv.org/abs/1905.05970

HOL4 https://kth-step.github.io/itppv-course/

HOL light

• wikpedia
• Harrison’s page
• tutorial quite good
• Thomas Hale - Formal Proof article Succinct summary of axioms
• #

Isabelle

from lcf to isabelle sel4 - verified microkernel

Metalevel is a syntax for describing inference rules

• !! x. \Lambda Universal variables at the meta level. enables Schema
• ==> is inference rule
• %x. is meta level lambda?

typeclasses vs locales

Sledgehammer: some history, some tips isabelle cookboook: programming in ML more isabelle ML programming notes

Baby examples

Isabelle => vs –> vs ==> => is the function type –> is implication ==> is meta implication, which is something like a sequent |-