CakeML: A Verified Implementation of ML
-
Updated
Nov 17, 2024 - Standard ML
CakeML: A Verified Implementation of ML
Hands-on Labs (HOLs) and presentations for Microservices, Serverless and Containers readiness.
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
Model finder for higher-order logic
[wip] A LCF-style kernel of trust intended for certified ATP and proof checking for FOL/HOL.
Scripts for deploying HOL Light with Docker (and optional checkpointing)
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.
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."