This bibliography is split into the following sections: some proof assistants; computer-checked proofs in English; more format converters and verifiers. Each section lists references in chronological order.
Some proof assistants
2002 Nipkow–Paulson–Wenzel: Isabelle/HOL.
2013 Bertot–Castéran: Coq, subsequently renamed Rocq.
2015 Bancerek–Bylinski–Grabowski–Kornilowicz–Matuszewski–Naumowicz–Pak–Urban: the core Mizar language.
2018 Bancerek–Bylinski–Grabowski–Kornilowicz–Matuszewski–Naumowicz–Pak: the Mizar math library.
2020 The mathlib community: the Lean math library.
2021 Moura–Ullrich: the Lean 4 language.
2023 Carneiro: an open-source reimplementation of Mizar.
Computer-checked proofs in English
1976 Chester described a program EXPOUND to convert inference sequences into English proofs.
1987 Felty–Miller described the χ-proof system, with extra information attached to inferences to improve presentation as English proofs.
1990 Cohn converted tactic sequences for HOL into English proofs.
1995 Coscoy–Kahn–Thery described a converter (part of ctcoq) to convert Coq inference sequences into English proofs, including various compression mechanisms.
1997 Coscoy presented further compression mechanisms.
1999 Holland-Minkley–Barzilay–Constable converted tactic sequences for Nuprl into English proofs.
2005 Cairns–Gow described a tool Maze to convert annotated Mizar proofs into English proofs.
2009 Cramer–Fisseni–Koepke–Kühlwein–Schröder–Veldman described Naproche, a system to computer-check some English proofs.
2013 Ganesalingam–Gowers described a tool to generate some types of proofs and convert them into English proofs.
2017 Bedford presented a tool Coqatoo to convert tactic sequences for Coq into English proofs.
More format converters and verifiers
1993 Wong presented a tool to record HOL88 inferences in a text format.
1995 Gordon–Herbert–Hale–Harrison–Wong–von Wright presented a tool to verify inferences recorded in that text format, and a proof that the algorithms used in the tool match a simpler description of inference verification.
1996 Wong presented a faster tool to verify inferences recorded in that text format. See also the journal version.
1996 Howe described a tool to import HOL Light statements (not proofs) into Nuprl.
2000 Denney described a prototype tool to import some HOL Light inferences (not definitions or type instantiations) into Coq.
2006 Obua–Skalberg
introduced ProofRecording to record HOL Light traces (this is maintained as part of the HOL Light distribution);
a similar tool for HOL4;
and a tool to replay ProofRecording files in Isabelle.
There are (as in Wong's format) two types of ProofRecording traces:
"BASIC" with only primitive inferences,
and "EXTENDED" with some higher-level inferences such as SYM.
2006 McLaughlin introduced a tool translating thousands of Isabelle proofs into HOL Light proofs.
2010 Keller–Werner added another HOL Light trace format to ProofRecording, and a tool to replay traces in that format inside Coq.
2011 Hurd presented OpenTheory as a format for HOL traces. The OpenTheory home page links to tools to record inferences from HOL Light, HOL4, and ProofPower in OpenTheory format, and tools to replay inferences in HOL Light, HOL4, ProofPower, and Isabelle. (The HOLTrace package now provides another way to replay OpenTheory traces in HOL Light, since it has a converter from OpenTheory format to HOLTrace format.)
2013 Kaliszyk–Krauss presented a more efficient format for HOL Light traces, and a tool to replay the traces in Isabelle.
2021 Kohlhase–Rabe surveyed work on exporting libraries from Coq, HOL Light, IMPS, Isabelle, Mizar, and PVS to a unified language, MMT.
2022 Abrahamsson presented an OpenTheory verifier (on top of Candle, on top of CakeML) with a proof that the machine code for the verifier allows only valid HOL theorems.
2024 Blanqui presented an export mechanism from HOL Light to Dedukti, and an import mechanism from Dedukti to Coq.
Version: This is version 2025.06.29 of the "Literature" web page.