seL4 specification and proofs
-
Updated
Apr 13, 2022 - Isabelle
#
isabelle
Here are 57 public repositories matching this topic...
A curated set of links to formal methods involving provable code.
-
Updated
Dec 12, 2021
Model finder for higher-order logic
-
Updated
Aug 25, 2021 - OCaml
An experimental implementation of homotopy type theory in the interactive proof assistant Isabelle
-
Updated
Jun 28, 2021 - Standard ML
An implementation of Hoare and He's Unifying Theories of Programming in Isabelle
-
Updated
Mar 21, 2022 - Isabelle
A Scala library for controlling/interacting with Isabelle
-
Updated
Mar 2, 2022 - Scala
Fully verified model checker for realtime systems
-
Updated
Mar 19, 2022 - Isabelle
A dependent type theory logic for Isabelle
dependent-types
proof-assistant
type-theory
isabelle
interactive-theorem-proving
logical-framework
dependent-type-theory
-
Updated
Feb 8, 2021 - Standard ML
A client for Isabelle server (https://isabelle.in.tum.de)
-
Updated
Apr 12, 2022 - TeX
Verifying the optimization phases of the GraalVM compiler
-
Updated
Apr 13, 2022 - Isabelle
Experiments in Isabelle/Pure (and a bit of HOL) (ARCHIVED)
-
Updated
Aug 10, 2018 - Standard ML
Exercises in the famous theorem prover
-
Updated
Apr 9, 2021 - Isabelle
QuickCheck-like testing framework for Isabelle/ML
-
Updated
Oct 8, 2021 - Standard ML
Propositional logic and FOL proofs (froward style)
-
Updated
Dec 2, 2017 - Isabelle
Semánticas de lenguajes de programación formalizadas en Isabelle/HOL
-
Updated
Jul 26, 2017 - Isabelle
ATMEGA32U4 code for the physical Sledgehammer device developed at TUM
-
Updated
Mar 8, 2018 - C++
Improve this page
Add a description, image, and links to the isabelle topic page so that developers can more easily learn about it.
Add this topic to your repo
To associate your repository with the isabelle topic, visit your repo's landing page and select "manage topics."