CakeML: A Verified Implementation of ML
-
Updated
Oct 30, 2024 - Standard ML
CakeML: A Verified Implementation of ML
Model finder for higher-order logic
An implementation of Hoare and He's Unifying Theories of Programming in Isabelle
Verilog development and verification project for HOL4
The opentheory tool processes higher order logic theory packages
Hands-on Labs (HOLs) and presentations for Microservices, Serverless and Containers readiness.
[wip] A LCF-style kernel of trust intended for certified ATP and proof checking for FOL/HOL.
A purely functional higher order logic kernel
Coq version of (part of) the HOL-IMP theories accompanying the book "Concrete Semantics with Isabelle/HOL". Formalized using a now outdated version of CoqHammer.
Local mirror of Featherweight OCL entry of the Archive of Formal Proofs (AFP).
Add a description, image, and links to the hol topic page so that developers can more easily learn about it.
To associate your repository with the hol topic, visit your repo's landing page and select "manage topics."