Isabelle Parallel Corpus

Contributing to the IPC

You can contribute to the IPC via github or via email. More details soon.

To contribute an entry in the parallel corpus, we ask that you provide the following:

• A copy of the natural language sentences that correspond to the statement of the problem you are working on;
• The title, bibtex citation or URL to the natural language source of the problem (e.g., textbook, paper for a statement and/or proof in natural language);
• A pointer to the AFP/Library entry for the artefact, if one exists;
• Some identification of those sentences in the natural language proof that helped you formalise a problem. This can take the form of a PDF (or a scan) with the sentences highlighted with a digital (or actual) highlighter.
• A code snippet of your Isabelle proof for the artefact

Your contributions to the IPC will be credited to you directly in (i) the "Hall of Contributors" section, (ii) on the github repository and (iii) in IPC public releases.