Email Gateway (Aug 18 2022 at 11:40): Email Gateway (Aug 18 2022 at 11:40):From: Christian Urban <urbanc@in.tum.de>
Hi,
There is already quite good documentation available for users to learn how to
interact with Isabelle and to use it for proving theorems. However, the entry
barrier for users to program on the ML-level of Isabelle is still unbearably
high. We have money to change this state of affairs and want to provide a cook
book about ML-coding in Isabelle.
If you familiar with the ML-level of Isabelle, then then we can offer money
for writing small parts of this documentation. Please get in contact with us.
If you are not familiar, but like to know more about the bits and pieces that
make up the Isabelle code, then let us know what you are interested in or what
project you like to implement. Above all we like to help future users and
developers of Isabelle; we do not want to end up with some "artificial
documentation" that is of nobody's help. We have outlined some possible
topics of interest at
http://isabelle.in.tum.de/nominal/activities/idp/
but we are more than welcome to the Isabelle community's input.
Best wishes,
Christian Urban
Larry Paulson
Michael Norrish
Last updated: May 03 2024 at 08:18 UTC