@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 = {Mathematical Quotients and Quotient Types in Coq},+ −
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}+ −