1 @inproceedings{Nogin02, |
|
2 author = {Aleksey Nogin}, |
|
3 title = {Quotient Types: A Modular Approach}, |
|
4 booktitle = {TPHOLs}, |
|
5 year = {2002}, |
|
6 pages = {263-280}, |
|
7 ee = {http://link.springer.de/link/service/series/0558/bibs/2410/24100263.htm}, |
|
8 crossref = {DBLP:conf/tphol/2002}, |
|
9 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
10 } |
|
11 @proceedings{DBLP:conf/tphol/2002, |
|
12 editor = {Victor Carre{\~n}o and |
|
13 C{\'e}sar Mu{\~n}oz and |
|
14 Sofi{\`e}ne Tahar}, |
|
15 title = {Theorem Proving in Higher Order Logics, 15th International |
|
16 Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, |
|
17 2002, Proceedings}, |
|
18 booktitle = {TPHOLs}, |
|
19 publisher = {Springer}, |
|
20 series = {Lecture Notes in Computer Science}, |
|
21 volume = {2410}, |
|
22 year = {2002}, |
|
23 isbn = {3-540-44039-9}, |
|
24 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
25 } |
|
26 |
|
27 @techreport{PVS:Interpretations, |
|
28 Author= {S. Owre and N. Shankar}, |
|
29 Title= {Theory Interpretations in PVS}, |
|
30 Number= {SRI-CSL-01-01}, |
|
31 Institution= {Computer Science Laboratory, SRI International}, |
|
32 Address= {Menlo Park, CA}, |
|
33 Month= {April}, |
|
34 Year= {2001}} |
|
35 |
|
36 @inproceedings{ChicliPS02, |
|
37 author = {Laurent Chicli and |
|
38 Loic Pottier and |
|
39 Carlos Simpson}, |
|
40 title = {Mathematical Quotients and Quotient Types in Coq}, |
|
41 booktitle = {TYPES}, |
|
42 year = {2002}, |
|
43 pages = {95-107}, |
|
44 ee = {http://link.springer.de/link/service/series/0558/bibs/2646/26460095.htm}, |
|
45 crossref = {DBLP:conf/types/2002}, |
|
46 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
47 } |
|
48 |
|
49 @proceedings{DBLP:conf/types/2002, |
|
50 editor = {Herman Geuvers and |
|
51 Freek Wiedijk}, |
|
52 title = {Types for Proofs and Programs, Second International Workshop, |
|
53 TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, |
|
54 Selected Papers}, |
|
55 booktitle = {TYPES}, |
|
56 publisher = {Springer}, |
|
57 series = {Lecture Notes in Computer Science}, |
|
58 volume = {2646}, |
|
59 year = {2003}, |
|
60 isbn = {3-540-14031-X}, |
|
61 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
62 } |
|
63 |
|
64 @article{Paulson06, |
|
65 author = {Lawrence C. Paulson}, |
|
66 title = {Defining functions on equivalence classes}, |
|
67 journal = {ACM Trans. Comput. Log.}, |
|
68 volume = {7}, |
|
69 number = {4}, |
|
70 year = {2006}, |
|
71 pages = {658-675}, |
|
72 ee = {http://doi.acm.org/10.1145/1183278.1183280}, |
|
73 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
74 } |
|
75 |
|
76 @inproceedings{Slotosch97, |
|
77 author = {Oscar Slotosch}, |
|
78 title = {Higher Order Quotients and their Implementation in Isabelle |
|
79 HOL}, |
|
80 booktitle = {TPHOLs}, |
|
81 year = {1997}, |
|
82 pages = {291-306}, |
|
83 ee = {http://dx.doi.org/10.1007/BFb0028401}, |
|
84 crossref = {DBLP:conf/tphol/1997}, |
|
85 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
86 } |
|
87 @proceedings{DBLP:conf/tphol/1997, |
|
88 editor = {Elsa L. Gunter and |
|
89 Amy P. Felty}, |
|
90 title = {Theorem Proving in Higher Order Logics, 10th International |
|
91 Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, |
|
92 1997, Proceedings}, |
|
93 booktitle = {TPHOLs}, |
|
94 publisher = {Springer}, |
|
95 series = {Lecture Notes in Computer Science}, |
|
96 volume = {1275}, |
|
97 year = {1997}, |
|
98 isbn = {3-540-63379-0}, |
|
99 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
100 } |
|
101 |
|
102 @inproceedings{Homeier05, |
|
103 author = {Peter V. Homeier}, |
|
104 title = {A Design Structure for Higher Order Quotients}, |
|
105 booktitle = {TPHOLs}, |
|
106 year = {2005}, |
|
107 pages = {130-146}, |
|
108 ee = {http://dx.doi.org/10.1007/11541868_9}, |
|
109 crossref = {DBLP:conf/tphol/2005}, |
|
110 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
111 } |
|
112 @proceedings{DBLP:conf/tphol/2005, |
|
113 editor = {Joe Hurd and |
|
114 Thomas F. Melham}, |
|
115 title = {Theorem Proving in Higher Order Logics, 18th International |
|
116 Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, |
|
117 Proceedings}, |
|
118 booktitle = {TPHOLs}, |
|
119 publisher = {Springer}, |
|
120 series = {Lecture Notes in Computer Science}, |
|
121 volume = {3603}, |
|
122 year = {2005}, |
|
123 isbn = {3-540-28372-2}, |
|
124 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
125 } |
|