Email Gateway (Aug 22 2022 at 15:04): Email Gateway (Aug 22 2022 at 15:04):From: Tobias Nipkow <nipkow@in.tum.de>
Differential Dynamic Logic
Brandon Bohrer
We formalize differential dynamic logic, a logic for proving properties of
hybrid systems. The proof calculus in this formalization is based on the uniform
substitution principle. We show it is sound with respect to our denotational
semantics, which provides increased confidence in the correctness of the
KeYmaera X theorem prover based on this calculus. As an application, we include
a proof term checker embedded in Isabelle/HOL with several example proofs.
Published in: Brandon Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Völp, André
Platzer: Formally verified differential dynamic logic. CPP 2017.
https://www.isa-afp.org/entries/Differential_Dynamic_Logic.shtml
Enjoy!
smime.p7s
Last updated: Oct 31 2025 at 12:44 UTC