Recycling proof patterns in Coq: case studies
From MaRDI portal
Publication:475385
DOI10.1007/s11786-014-0173-1zbMath1302.68243arXiv1301.6039OpenAlexW2071091648MaRDI QIDQ475385
Jónathan Heras, Ekaterina Komendantskaya
Publication date: 26 November 2014
Published in: Mathematics in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1301.6039
Related Items
Deepalgebra -- an outline of a program ⋮ Proof mining with dependent types ⋮ JEFL: joint embedding of formal proof libraries ⋮ Deep Generation of Coq Lemma Names Using Elaborated Terms ⋮ Aligning concepts across proof assistant libraries ⋮ Recycling proof patterns in Coq: case studies ⋮ TacticToe: learning to prove with tactics
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Conjecture synthesis for inductive theories
- 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.
- A constructive approach to sequential Nash equilibria
- Learning Boolean functions in an infinite attribute space
- Isabelle/HOL. A proof assistant for higher-order logic
- A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory
- Proof-Pattern Recognition and Lemma Discovery in ACL2
- Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
- A Brief Overview of Agda – A Functional Language with Dependent Types
- Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence
- Type classes for efficient exact real arithmetic in Coq
- The Matita Interactive Theorem Prover
- A Machine-Checked Proof of the Odd Order Theorem
- A verified information-flow architecture
- Rippling: Meta-Level Guidance for Mathematical Reasoning
- Types for Proofs and Programs
