@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= {{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 = {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}+ −
}+ −
+ −
@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+ −
}+ −