|
Please send your submission
via this web page.
You will need to supply the following information:
- Title, authors and abstract in plain text.
- A short name. It will become the directory name of the archive
entry.
- Name/contact of the maintainer of the entry (usually the author).
- URL or email address of authors to display on the web page.
- The topic(s) the entry should be listed under in the index.
- A tar file with the theory files, ROOT file, and
document directory. The theories should work with the current
release of Isabelle.
- A notice whether you license your submission under BSD
or LGPL if accepted. For LGPL submissions, please include the
header "License: LGPL" in each file.
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 afp-submit@in.tum.de.
The submission must follow the following Isabelle style rules.
For additional guidelines on Isabelle proofs, also see the this guide (feel free to follow all of these; only the below are mandatory).
- No use of the commands
sorry or back.
- Instantiations must not use Isabelle-generated names such as
xa — use Isar or rename_tac to avoid
such names.
- No use of the command
smt. The result of this
command depends on external tools that are not under our control and
may stop working in the future.
apply scripts should be indented by subgoal as in
the Isabelle distribution. If an apply command is
applied to a state with n+1 subgoals, it must be
indented by n spaces relative to the first
apply in the sequence.- Only named lemmas should carry attributes such as
[simp].
- We prefer structured Isar proofs over apply style, but do not
mandate them.
- If there are proof steps that take significant time, i.e. longer
than roughly 1 min, please add a short comment to that step, so
maintainers will know what to expect.
There is an
example submission
that contains further information.
It is possible and encouraged to build on other archive entries
in your submission. There is a standardised way to
refer to other AFP entries in your
theories.
Your submission will be refereed and you will receive notification
as soon as possible. If accepted, you must agree to maintain your
archive entry or nominate someone else to maintain it. The Isabelle
development team will assist with maintenance, but it does not have the
resources to fully maintain the complete archive.
If you have questions regarding your submission, please email afp-submit@in.tum.de.
If you need help with Isabelle, please use the
isabelle-users@cl.cam.ac.uk
mailing list. It is always a good idea to subscribe.
|