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. 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.

An early proposed design and theory for Kaisar are available on arXiv. Using the insights gained from this work, a ground-up redesign is underway as part of my thesis work.

Example Proof in Experimental Kaisar Syntax

Related Publication(s)

Brandon Bohrer and André Platzer.
Toward Structured Proofs for Dynamic Logics arXiv, proposed design