Deep Generation of Coq Lemma Names Using Elaborated Terms

DOI10.1007/978-3-030-51054-1_6OpenAlexW3046547863MaRDI QIDQ5048996

Pengyu Nie, Karl Palmskog, Junyi Jessy Li, Miloš V. Gligorić

Publication date: 9 November 2022

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2004.07761

zbMATH Keywords

neural networksproof assistantsCoqlemma names

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

Roosterize

Uses Software

• Coq
• ML4PG
• HoTT
• Lean
• PyTorch
• Adam
• GitHub
• Lucene
• OpenNMT
• Archive Formal Proofs
• BLEU
• JSNice
• PCM library

Cites Work

• Unnamed Item
• Unnamed Item
• Recycling proof patterns in Coq: case studies
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Autarkic computations in formal proofs
• Regular language representations in the constructive type theory of Coq
• The Coq library as a theory graph
• Predicting Program Properties from "Big Code"
• What’s in a Theorem Name?
• ML4PG in Computer Algebra Verification
• A Formal Library for Elliptic Curves in the Coq Proof Assistant
• Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory
• Recursive functions of symbolic expressions and their computation by machine, Part I
• Mining the Archive of Formal Proofs
• The Lean Theorem Prover (System Description)
• A Machine-Checked Proof of the Odd Order Theorem

This page was built for publication: Deep Generation of Coq Lemma Names Using Elaborated Terms