Ornaments for Proof Reuse in Coq (Q5875438): Difference between revisions

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