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