@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}