Ornaments for Proof Reuse in Coq

DOI10.4230/LIPIcs.ITP.2019.26OpenAlexW2978136495MaRDI QIDQ5875438

Dan Grossman, Nathaniel Yazdani, John W. Leo, Talia Ringer

Publication date: 3 February 2023

Full work available at URL: https://dblp.uni-trier.de/db/conf/itp/itp2019.html#RingerYLG19

zbMATH Keywords

proof automationornamentsproof reuse

Mathematics Subject Classification ID

Uses Software

• Coq
• Ghostbuster
• Transfer
• Lifting
• cubicaltt
• GitHub

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• First Steps Towards Cumulative Inductive Types in CIC
• Proofs for free
• Transporting functions across ornaments
• Meta-theory à la carte
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Ghostbuster: a tool for simplifying and converting GADTs
• Changing Data Representation within the Coq System
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Tactic theorem proving with refinement-tree proofs and metavariables
• A Categorical Treatment of Ornaments
• Programming with ornaments
• The essence of ornaments
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Theorem Proving in Higher Order Logics
• Equations: A Dependent Pattern-Matching Compiler

This page was built for publication: Ornaments for Proof Reuse in Coq