Un corpus parallèle est un ensemble de textes dans une langue associés à des textes correspondants dans une autre langue.

Le Corpus Parallèle Isabelle (IPC) est une initiative communautaire visant à créer un corpus parallèle de documents Isabelle. L'IPC associe des documents formels dans Isabelle (tels que des théorèmes, des lemmes, des définitions, etc.) à leurs homologues en langage naturel.

Les entrées dans l’IPC ont plusieurs niveaux d’annotation de données. Au premier niveau, les énoncés en langage naturel des documents (par exemple, les énoncés de théorèmes) et les sources en langage naturel (par exemple, les manuels scolaires) sont enregistrés. Le deuxième niveau d'annotation associe des phrases de la preuve en langage naturel avec des instructions du script de preuve Isabelle correspondant. Le troisième niveau d'annotation permet d'aligner les mots du langage naturel avec les jetons du script de preuve Isabelle.