--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Quotient-Paper-jv/document/root.bib Tue Dec 20 17:54:53 2011 +0900
@@ -0,0 +1,203 @@
+@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