Kaisar Structured Proof Language

Proof assistants hold great promise for giving us certainty where certainty is needed, but their drawback has always been the difficulty of learning and using them, reducing productivity even for experienced users. One way to address this is by targeting an interface between the user and prover, such as the proof scripting language. The Isar structured proof language for higher-order logics, part of Isabelle, struck on a style of proof that significantly improves the readability and maintainability of proofs in higher-order logic.

However, not all logics are higher-order logics. In particular, we use a dynamic logic called differential dynamic logic to verify hybrid systems in KeYmaera X. This family of logics has been extended with features like constructivity and games (CdGL). Thus, the goal of Kaisar is to take the gains made by Isar and extend them with new insights specific to dynamic logic in order to provide the same convenience for dynamic logics that Isar provides for higher-order logics. Kaisar is implemented for (CdGL), but its ideas apply to other logics too.

Paper

Rose Bohrer and André Platzer.
Structured Proofs for Adversarial Cyber-Physical Systems
21st International Conference on Embedded Software
EMSOFT 2021, The Internet, October 10-15, 2021, IEEE, 2021. © The authors.
To appear (in ACM TECS). preprint very old proposal