diff -r fb201e383f1b -r da575186d492 Quotient-Paper-jv/document/root.bib --- a/Quotient-Paper-jv/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