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

@@ label / en / label / en @@
+Ornaments for Proof Reuse in Coq
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://dblp.uni-trier.de/db/conf/itp/itp2019.html#RingerYLG19
+Normal rank
@@ Property / OpenAlex ID @@
+W2978136495
@@ Property / OpenAlex ID: W2978136495 / rank @@
+Normal rank
@@ Property / title @@
+Ornaments for Proof Reuse in Coq (English)
@@ Property / title: Ornaments for Proof Reuse in Coq (English) / rank @@
+Normal rank
@@ 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
@@ links / mardi / name / links / mardi / name @@
+Publication:5875438