Ein Parallelkorpus ist eine Sammlung von Texten in einer Sprache, gepaart mit entsprechenden Texten in einer anderen Sprache.

Das Isabelle Parallel Corpus (IPC) ist eine Community-gesteuerte Initiative zur Erstellung eines parallelen Korpus von Isabelle-Dokumenten. IPC koppelt formale Dokumente in Isabelle (wie Theoreme, Lemmata, Definitionen usw.) mit ihren Gegenstücken in natürlicher Sprache.

Einträge im IPC verfügen über mehrere Ebenen der Datenannotation. Auf der ersten Ebene werden natürlichsprachliche Aussagen von Dokumenten (z. B. Theoremaussagen) und natürlichsprachlichen Quellen (z. B. Lehrbücher) erfasst. Die zweite Annotationsebene paart Sätze im Beweis in natürlicher Sprache mit Aussagen im entsprechenden Isabelle-Beweisskript. Die dritte Annotationsebene ermöglicht die Ausrichtung von Wörtern in der natürlichen Sprache mit Token im Isabelle-Beweisskript.