A formally verified implementation of differential dynamic logic in Isabelle
Isabelle TeX
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
Word_Lib
document
.gitignore
Axioms.thy
Bound_Effect.thy
Codegen-Exploder.thy
Codegen_Example.thy
Codegen_Exploder.thy
Coincidence.thy
Denotational_Semantics.thy
Differential_Axioms.thy
Differential_Dynamic_Logic.thy
Example_DIAnd.thy
Example_System.thy
Frechet_Correctness.thy
Ids.thy
Interval_Arithmetic.thy
Lib.thy
Lib.thy~
Old_proofchecker.thy
Pretty_Printer.thy
Proof_Checker.thy
README.md
ROOT
Scratch.thy
Static_Semantics.thy
Syntax.thy
USubst.thy
USubst_Lemma.thy
Uniform_Renaming.thy

README.md

Formalization of Differential Dynamic Logic

This formalization defines a deep embedding of differential dynamic logic and proves it sound. We support a significant fragment of operations supported in the KeYmaera X theorem prover, and non-trivial proofs can be exported from KeYmaera X and rechecked with the formalized system. The formalization also provides an alternative (computable) integer interval semantics for dL and a soundness theorem with respect to the standard semantics.

This repository contains the most recent (and therefore least stable) changes. At times, it may only check with development versions of Isabelle. For a more stable but less developed copy, see:

https://www.isa-afp.org/entries/Differential_Dynamic_Logic.html