hol4

There are 10 repositories under hol4 topic.

AeneasVerif/aeneas
A verification toolchain for Rust programs
Language:OCaml376 6 19835
kth-step/HolBA
Binary analysis in HOL
Language:Standard ML42 4 4921
kth-step/HOL4P4
P4 formalization using Ott and HOL4
Language:Standard ML12 5 10
kth-step/itppv-course
Interactive Theorem Proving course using HOL4
Language:Standard ML11 5 00
palmskog/fitch
Certified proof checker for Fitch-style propositional logic proofs
Language:Standard ML7 3 12
kth-step/mil
Formal definition, metatheory, and tools for the Machine Independent Language using HOL4 and CakeML
Language:Standard ML2 4 00
rse-verification/contract-compositionality
HOL4 formalization of a theory of specifications, components, contracts, and compositionality
Language:Standard ML0 2 00
kth-step/step-hol-utils
Utility functions and tactics for HOL4
Language:Standard ML4 0
totorigolo/kth-hol4-exercises
My solutions for the KTH HOL4 course - Interactive Theorem Proving
Language:Standard ML1 0
tupipa/hol4-docker
Dockerfiles to build HOL4 (https://github.com/HOL-Theorem-Prover/HOL)
Language:Standard ML1 0