--- a/src/Doc/manual.bib Tue Jul 30 23:17:26 2013 +0200
+++ b/src/Doc/manual.bib Wed Jul 31 11:28:59 2013 +0200
@@ -301,6 +301,12 @@
author = "Jasmin Christian Blanchette and Tobias Nipkow",
crossref = {itp2010}}
+@unpublished{blanchette-et-al-wit,
+ author = {J.C. Blanchette and A. Popescu and D. Traytel},
+ title = {Witnessing (Co)datatypes},
+ year = 2013,
+ note = {\url{http://www21.in.tum.de/~traytel/papers/witness/wit.pdf}}}
+
@inproceedings{why3,
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and Claude March\'e and Andrei Paskevich},
title = {{Why3}: Shepherd Your Herd of Provers},
@@ -1662,7 +1668,16 @@
Subtyping (long version)},
year = 2011,
note = {Submitted,
- \url{http://isabelle.in.tum.de/doc/implementation.pdf}}},
+ \url{http://isabelle.in.tum.de/doc/implementation.pdf}}}
+
+@inproceedings{traytel-et-al-2012,
+ author = "Dmitriy Traytel and Andrei Popescu and Jasmin Christian Blanchette",
+ title = {Foundational, Compositional (Co)datatypes for Higher-Order
+ Logic---{C}ategory Theory Applied to Theorem Proving},
+ year = {2012},
+ pages = {596--605},
+ booktitle = {LICS 2012},
+ publisher = {IEEE}
}
@Unpublished{Trybulec:1993:MizarFeatures,