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

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 |-