Deep Generation of Coq Lemma Names Using Elaborated Terms
From MaRDI portal
Publication:5048996
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
Related Items (1)
Uses Software
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
