Extracting ω's programs from proofs in the calculus of constructions

By Christine Paulin-Mohring. 1989

Subfields: Prompting & Reasoning

How researchers see this paper

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

In Prompting & Reasoning

1. Stella Biderman
2. Albert Qiaochu Jiang
3. Zhangir Azerbayev
4. Sean Welleck
5. Keiran Paster

Citations in the corpus

• Llemma: An Open Language Model For Mathematics (2023, background): “Interactive proof assistants such as Lean (de Moura et al., 2015), Isabelle (Wenzel et al., 2008), and Coq (Paulin-Mohring, 1989a;b) express mathematics in programming languages that allow for verification.”