The coq proof assistant reference manual

By G. Huet, Christine Paulin-Mohring. 2000

1,211 citations recorded by the source corpus.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

1. Daniel Whalen
2. Mingzhe Wang
3. Stanislas Polu
4. Jesse Michael Han
5. Kunhao Zheng
6. Jia Deng
7. Cezary Kaliszyk

Citations in the corpus

• Holophrasm: a neural Automated Theorem Prover for higher-order logic (2016, methodology): “Large datasets of formal proofs include Metamath [1], the Mizar Mathematical Library [2], Flyspeck [3], the Archive of Formal Proofs [4], the Coq standard library [5], and the HOL Light library [6].”
• A Survey of Deep Learning for Mathematical Reasoning (2022, unknown): “…there has been increased interest in using language models for theorem proving in formal interactive theorem provers (ITP) (e.g., Polu and Sutskever (2020) Example ITPs include Lean (Moura et al., 2015), Isabelle (Paulson, 1994), Coq (Barras et al., 1999), and Metamath (Megill and Wheeler, 2019).”