--- a/Quotient-Paper/document/root.bib Tue Feb 19 05:38:46 2013 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,203 +0,0 @@
-@inproceedings{Nogin02,
- author = {Aleksey Nogin},
- title = {Quotient Types: A Modular Approach},
- booktitle = {Proc.~of the 15th TPHOLs conference},
- year = {2002},
- pages = {263-280},
- series = {LNCS},
- volume = {2646}
-}
-
-@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= {{T}heory {I}nterpretations 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 = {{M}athematical {Q}uotients and {Q}uotient {T}ypes in {C}oq},
- booktitle = {Proc of the TYPES workshop},
- year = {2002},
- pages = {95-107},
- series = {LNCS},
- volume = {2646}
-}
-
-@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 = {Proc.~of the 10th TPHOLs conference},
- year = {1997},
- pages = {291-306},
- series = {LNCS},
- volume = {1275}
-}
-
-@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 = {Proc of the 18th TPHOLs conference},
- year = {2005},
- pages = {130-146},
- series = {LNCS},
- volume = {3603}
-}
-
-@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}
-}
-
-@BOOK{harrison-thesis,
- author = "John Harrison",
- title = "Theorem Proving with the Real Numbers",
- publisher = "Springer-Verlag",
- year = 1998}
-
-@BOOK{Barendregt81,
- AUTHOR = "H.~Barendregt",
- TITLE = "{T}he {L}ambda {C}alculus: {I}ts {S}yntax and {S}emantics",
- PUBLISHER = "North-Holland",
- YEAR = 1981,
- VOLUME = 103,
- SERIES = "Studies in Logic and the Foundations of Mathematics"
-}
-
-@BOOK{CurryFeys58,
- AUTHOR = "H.~B.~Curry and R.~Feys",
- TITLE = "{C}ombinatory {L}ogic",
- PUBLISHER = "North-Holland",
- YEAR = "1958",
- VOLUME = 1,
- SERIES = "Studies in Logic and the Foundations of Mathematics"
-}
-
-@Unpublished{UrbanKaliszyk11,
- author = {C.~Urban and C.~Kaliszyk},
- title = {{G}eneral {B}indings and {A}lpha-{E}quivalence in {N}ominal {I}sabelle},
- note = {submitted for publication},
- month = {July},
- year = {2010},
-}
-
-@InProceedings{BengtsonParrow07,
- author = {J.~Bengtson and J.~Parrow},
- title = {Formalising the pi-{C}alculus using {N}ominal {L}ogic},
- booktitle = {Proc.~of the 10th FOSSACS Conference},
- year = 2007,
- pages = {63--77},
- series = {LNCS},
- volume = {4423}
-}
-
-@inproceedings{BengtsonParow09,
- author = {J.~Bengtson and J.~Parrow},
- title = {{P}si-{C}alculi in {I}sabelle},
- booktitle = {Proc of the 22nd TPHOLs Conference},
- year = 2009,
- pages = {99--114},
- series = {LNCS},
- volume = {5674}
-}
-
-@inproceedings{TobinHochstadtFelleisen08,
- author = {S.~Tobin-Hochstadt and M.~Felleisen},
- booktitle = {Proc.~of the 35rd POPL Symposium},
- title = {{T}he {D}esign and {I}mplementation of {T}yped {S}cheme},
- publisher = {ACM},
- year = {2008},
- pages = {395--406}
-}
-
-@InProceedings{UrbanCheneyBerghofer08,
- author = "C.~Urban and J.~Cheney and S.~Berghofer",
- title = "{M}echanizing the {M}etatheory of {LF}",
- pages = "45--56",
- year = 2008,
- booktitle = "Proc.~of the 23rd LICS Symposium"
-}
-
-@InProceedings{UrbanZhu08,
- title = "{R}evisiting {C}ut-{E}limination: {O}ne {D}ifficult {P}roof is {R}eally a {P}roof",
- author = "C.~Urban and B.~Zhu",
- booktitle = "Proc.~of the 9th RTA Conference",
- year = "2008",
- pages = "409--424",
- series = "LNCS",
- volume = 5117
-}
\ No newline at end of file