kth-step/itppv-course

Interactive Theorem Proving course using HOL4

FDD3023 Interactive Theorem Proving and Program Verification

See the course website at: https://kth-step.github.io/itppv-course/

See also supplementary files for homeworks.

The following files are licensed under the CC-BY-SA license and derived from Thomas Tuerk's ITP Course material:

• philScript.sml
• dot_graphsLib.sig
• dot_graphsLib.sml
• hw4ArraysLib.sml
• hw4ArraysScript.sml