The purpose of this post is to explain how KeYmaera X users can distribute their artifacts to reviewers and readers via the publicly accessible instance of KeYmaera X. The tool is also useful for notes, blog posts, course materials, etc. – basically, any time you have a KeYmaera X model/proof that you want to share with a wide audience.

From a reader’s or reviewer’s perspective, the process is painless. They create an account on our public instance (or, if they wish, download/install KeYmaera X on their local machine). They then use our import tool to import the published case study files. Once the case study files are imported, the reviewer can read the model file and re-run any proofs supplied by the author, incuding partial proofs. In a separate note, I provide a detailed step-by-step tutorial for readers and reviewers.

To use our import tool as an author, you will need a public web host where you can store three files:

  • Your theorems (.kyx files)
  • Your Bellerophon tactics (.kyt files)
  • A JSON file

The JSON file should have the following format:

{
  "name": "Name Of Your Case Study (e.g., the title of your paper or blog post)",
  "entries": [
    {
      "name": "Name of Theorem",
      "description": "A description of this theorem",
      "title": "Title goes here",
      "link": "https://arxiv.org/abs/123.45678",
      "model": "http://link/to/model/file/goes/here.kyx",
      "tactic": "http://link/to/tactic/file/goes/here.kyt",
      "proves": true
    }
    ...more models can go here
  ]
}

A complete example case study is available here.

A few pieces of advice:

  • After the user imports your case study, the model files will appear on that user’s “Models” page. Therefore, choose good “name” values! For example, if you’re publishing a paper in HSCC, a good title might be “HSCC 20xx – your last name et al. – theorem name goes here”.
  • Similarly, choose good titles and descriptions.
  • The “proves” flag can be set to false. This is sometimes useful if you would like to provide access to a failed conjecture – especially if KeYmaera X produces a nice counter-example.