--- a/Quotient-Paper/document/root.bib~ Tue May 18 11:46:58 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,125 +0,0 @@
-@inproceedings{Nogin02,
- author = {Aleksey Nogin},
- title = {Quotient Types: A Modular Approach},
- booktitle = {TPHOLs},
- year = {2002},
- pages = {263-280},
- ee = {http://link.springer.de/link/service/series/0558/bibs/2410/24100263.htm},
- crossref = {DBLP:conf/tphol/2002},
- bibsource = {DBLP, http://dblp.uni-trier.de}
-}
-@proceedings{DBLP:conf/tphol/2002,
- editor = {Victor Carre{\~n}o and
- C{\'e}sar Mu{\~n}oz and
- Sofi{\`e}ne Tahar},
- title = {Theorem Proving in Higher Order Logics, 15th International
- Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23,
- 2002, Proceedings},
- booktitle = {TPHOLs},
- publisher = {Springer},
- series = {Lecture Notes in Computer Science},
- volume = {2410},
- year = {2002},
- isbn = {3-540-44039-9},
- bibsource = {DBLP, http://dblp.uni-trier.de}
-}
-
-@techreport{PVS:Interpretations,
- Author= {S. Owre and N. Shankar},
- Title= {Theory Interpretations in PVS},
- Number= {SRI-CSL-01-01},
- Institution= {Computer Science Laboratory, SRI International},
- Address= {Menlo Park, CA},
- Month= {April},
- Year= {2001}}
-
-@inproceedings{ChicliPS02,
- author = {Laurent Chicli and
- Loic Pottier and
- Carlos Simpson},
- title = {Mathematical Quotients and Quotient Types in Coq},
- booktitle = {TYPES},
- year = {2002},
- pages = {95-107},
- ee = {http://link.springer.de/link/service/series/0558/bibs/2646/26460095.htm},
- crossref = {DBLP:conf/types/2002},
- bibsource = {DBLP, http://dblp.uni-trier.de}
-}
-
-@proceedings{DBLP:conf/types/2002,
- editor = {Herman Geuvers and
- Freek Wiedijk},
- title = {Types for Proofs and Programs, Second International Workshop,
- TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002,
- Selected Papers},
- booktitle = {TYPES},
- publisher = {Springer},
- series = {Lecture Notes in Computer Science},
- volume = {2646},
- year = {2003},
- isbn = {3-540-14031-X},
- bibsource = {DBLP, http://dblp.uni-trier.de}
-}
-
-@article{Paulson06,
- author = {Lawrence C. Paulson},
- title = {Defining functions on equivalence classes},
- journal = {ACM Trans. Comput. Log.},
- volume = {7},
- number = {4},
- year = {2006},
- pages = {658-675},
- ee = {http://doi.acm.org/10.1145/1183278.1183280},
- bibsource = {DBLP, http://dblp.uni-trier.de}
-}
-
-@inproceedings{Slotosch97,
- author = {Oscar Slotosch},
- title = {Higher Order Quotients and their Implementation in Isabelle
- HOL},
- booktitle = {TPHOLs},
- year = {1997},
- pages = {291-306},
- ee = {http://dx.doi.org/10.1007/BFb0028401},
- crossref = {DBLP:conf/tphol/1997},
- bibsource = {DBLP, http://dblp.uni-trier.de}
-}
-@proceedings{DBLP:conf/tphol/1997,
- editor = {Elsa L. Gunter and
- Amy P. Felty},
- title = {Theorem Proving in Higher Order Logics, 10th International
- Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22,
- 1997, Proceedings},
- booktitle = {TPHOLs},
- publisher = {Springer},
- series = {Lecture Notes in Computer Science},
- volume = {1275},
- year = {1997},
- isbn = {3-540-63379-0},
- bibsource = {DBLP, http://dblp.uni-trier.de}
-}
-
-@inproceedings{Homeier05,
- author = {Peter V. Homeier},
- title = {A Design Structure for Higher Order Quotients},
- booktitle = {TPHOLs},
- year = {2005},
- pages = {130-146},
- ee = {http://dx.doi.org/10.1007/11541868_9},
- crossref = {DBLP:conf/tphol/2005},
- bibsource = {DBLP, http://dblp.uni-trier.de}
-}
-@proceedings{DBLP:conf/tphol/2005,
- editor = {Joe Hurd and
- Thomas F. Melham},
- title = {Theorem Proving in Higher Order Logics, 18th International
- Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005,
- Proceedings},
- booktitle = {TPHOLs},
- publisher = {Springer},
- series = {Lecture Notes in Computer Science},
- volume = {3603},
- year = {2005},
- isbn = {3-540-28372-2},
- bibsource = {DBLP, http://dblp.uni-trier.de}
-}