First stab at documenting Canonical Structures

1 files changed, 36 insertions, 0 deletions

diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib
index 3715c4c79..a2895cfcf 100644
--- a/doc/refman/biblio.bib
+++ b/doc/refman/biblio.bib
@@ -1291,3 +1291,39 @@ Languages},
     pages = "102--114",
     year = "1992",
 }
+
+@inproceedings{CSwcu,
+    hal_id = {hal-00816703},
+    url = {http://hal.inria.fr/hal-00816703},
+    title = {{Canonical Structures for the working Coq user}},
+    author = {Mahboubi, Assia and Tassi, Enrico},
+    booktitle = {{ITP 2013, 4th Conference on Interactive Theorem Proving}},
+    publisher = {Springer},
+    pages = {19-34},
+    address = {Rennes, France},
+    volume = {7998},
+    editor = {Sandrine Blazy and Christine Paulin and David Pichardie },
+    series = {LNCS },
+    doi = {10.1007/978-3-642-39634-2\_5 },
+    year = {2013},
+}
+
+@article{CSlessadhoc,
+ author = {Gonthier, Georges and Ziliani, Beta and Nanevski, Aleksandar and Dreyer, Derek},
+ title = {How to Make Ad Hoc Proof Automation Less Ad Hoc},
+ journal = {SIGPLAN Not.},
+ issue_date = {September 2011},
+ volume = {46},
+ number = {9},
+ month = sep,
+ year = {2011},
+ issn = {0362-1340},
+ pages = {163--175},
+ numpages = {13},
+ url = {http://doi.acm.org/10.1145/2034574.2034798},
+ doi = {10.1145/2034574.2034798},
+ acmid = {2034798},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {canonical structures, coq, custom proof automation, hoare type theory, interactive theorem proving, tactics, type classes},
+}