AFP Submission


Submission Guidelines

(Jump to submission form)

The submission must build with the current Isabelle release version. Submissions for older Isabelle versions are not accepted.

Submissions for the Isabelle development version are also acceptable, but publication of the entry on the front page will be deferred until the next Isabelle release. In the meantime the entry will only be visible on the development pages. In this case, submit your article as described above. Because your article is tested against the release version, this will fail (otherwise your article does not need the development version!) and you cannot perform the final step in the submission process. When that happens, simply copy the url of the submission page at that point into an email to

To submit your contribution, you need to create a zip or tar archive containing all your theories, including a ROOT file. All files need to reside in a folder that has the same name as the short article name (see below). When submitting multiple entries at once, there must be one entry per folder and one ROOT file per entry. If you don't already have a ROOT file, refer to the system manual for how to create one.

There is also a self-contained example submission that contains further information, including the structure of the entry and its ROOT file.

Hide guidelines



Title of article:
Example: Example Submission
Short article name (folder name):
Example: Example_Submission (name of the folder where your ROOT and theory files reside)
Example: Gerwin Klein <>, Johannes Hölzl <>
Example: Computer science/Security, Computer science/Programming languages/Type systems
(Index of topics)
Note: For LGPL submissions, please include the header "License: LGPL" in each file
Note: You can use HTML (not LaTeX!) to format your abstract.

Remove this entry


You can submit multiple entries at once. Put the corresponding folders in the archive and use the button below to add more input fields for metadata.

Add new entry


Example:, (These addresses serve two purposes: 1. They are used to send you updates about the state of your submission. 2. They are the maintainers of the entry once it is accepted. Typically this will be one or more of the authors. You can supply multiple addresses seperated by commas.)
Message for the editors:

Note: Anything special or noteworthy about your submission can be covered here. It will not become part of your entry. You're also welcome to leave suggestions for our AFP submission service here. (Can be left empty)
Archive file (.tar.gz or .zip):
Note: Your zip or tar file should contain one folder with your theories, ROOT, etc. The folder name should be the short/folder name used in the submission form.