2154
|
1 |
@inproceedings{Nogin02,
|
|
2 |
author = {Aleksey Nogin},
|
|
3 |
title = {Quotient Types: A Modular Approach},
|
2554
|
4 |
booktitle = {Proc.~of the 15th TPHOLs conference},
|
2154
|
5 |
year = {2002},
|
|
6 |
pages = {263-280},
|
2554
|
7 |
series = {LNCS},
|
|
8 |
volume = {2646}
|
2154
|
9 |
}
|
2554
|
10 |
|
2154
|
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},
|
2205
|
29 |
Title= {{T}heory {I}nterpretations in {PVS}},
|
2154
|
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},
|
2226
|
40 |
title = {{M}athematical {Q}uotients and {Q}uotient {T}ypes in {C}oq},
|
2554
|
41 |
booktitle = {Proc of the TYPES workshop},
|
2154
|
42 |
year = {2002},
|
|
43 |
pages = {95-107},
|
2554
|
44 |
series = {LNCS},
|
|
45 |
volume = {2646}
|
2154
|
46 |
}
|
|
47 |
|
|
48 |
@proceedings{DBLP:conf/types/2002,
|
|
49 |
editor = {Herman Geuvers and
|
|
50 |
Freek Wiedijk},
|
|
51 |
title = {Types for Proofs and Programs, Second International Workshop,
|
|
52 |
TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002,
|
|
53 |
Selected Papers},
|
|
54 |
booktitle = {TYPES},
|
|
55 |
publisher = {Springer},
|
|
56 |
series = {Lecture Notes in Computer Science},
|
|
57 |
volume = {2646},
|
|
58 |
year = {2003},
|
|
59 |
isbn = {3-540-14031-X},
|
|
60 |
bibsource = {DBLP, http://dblp.uni-trier.de}
|
|
61 |
}
|
|
62 |
|
|
63 |
@article{Paulson06,
|
|
64 |
author = {Lawrence C. Paulson},
|
|
65 |
title = {Defining functions on equivalence classes},
|
|
66 |
journal = {ACM Trans. Comput. Log.},
|
|
67 |
volume = {7},
|
|
68 |
number = {4},
|
|
69 |
year = {2006},
|
|
70 |
pages = {658-675},
|
|
71 |
ee = {http://doi.acm.org/10.1145/1183278.1183280},
|
|
72 |
bibsource = {DBLP, http://dblp.uni-trier.de}
|
|
73 |
}
|
|
74 |
|
|
75 |
@inproceedings{Slotosch97,
|
|
76 |
author = {Oscar Slotosch},
|
|
77 |
title = {Higher Order Quotients and their Implementation in Isabelle
|
|
78 |
HOL},
|
2554
|
79 |
booktitle = {Proc.~of the 10th TPHOLs conference},
|
2154
|
80 |
year = {1997},
|
|
81 |
pages = {291-306},
|
2554
|
82 |
series = {LNCS},
|
|
83 |
volume = {1275}
|
2154
|
84 |
}
|
2554
|
85 |
|
2154
|
86 |
@proceedings{DBLP:conf/tphol/1997,
|
|
87 |
editor = {Elsa L. Gunter and
|
|
88 |
Amy P. Felty},
|
|
89 |
title = {Theorem Proving in Higher Order Logics, 10th International
|
|
90 |
Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22,
|
|
91 |
1997, Proceedings},
|
|
92 |
booktitle = {TPHOLs},
|
|
93 |
publisher = {Springer},
|
|
94 |
series = {Lecture Notes in Computer Science},
|
|
95 |
volume = {1275},
|
|
96 |
year = {1997},
|
|
97 |
isbn = {3-540-63379-0},
|
|
98 |
bibsource = {DBLP, http://dblp.uni-trier.de}
|
|
99 |
}
|
|
100 |
|
|
101 |
@inproceedings{Homeier05,
|
|
102 |
author = {Peter V. Homeier},
|
|
103 |
title = {A Design Structure for Higher Order Quotients},
|
2554
|
104 |
booktitle = {Proc of the 18th TPHOLs conference},
|
2154
|
105 |
year = {2005},
|
|
106 |
pages = {130-146},
|
2554
|
107 |
series = {LNCS},
|
|
108 |
volume = {3603}
|
2154
|
109 |
}
|
2554
|
110 |
|
2154
|
111 |
@proceedings{DBLP:conf/tphol/2005,
|
|
112 |
editor = {Joe Hurd and
|
|
113 |
Thomas F. Melham},
|
|
114 |
title = {Theorem Proving in Higher Order Logics, 18th International
|
|
115 |
Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005,
|
|
116 |
Proceedings},
|
|
117 |
booktitle = {TPHOLs},
|
|
118 |
publisher = {Springer},
|
|
119 |
series = {Lecture Notes in Computer Science},
|
|
120 |
volume = {3603},
|
|
121 |
year = {2005},
|
|
122 |
isbn = {3-540-28372-2},
|
|
123 |
bibsource = {DBLP, http://dblp.uni-trier.de}
|
|
124 |
}
|
|
125 |
|
|
126 |
@BOOK{harrison-thesis,
|
|
127 |
author = "John Harrison",
|
|
128 |
title = "Theorem Proving with the Real Numbers",
|
|
129 |
publisher = "Springer-Verlag",
|
2220
|
130 |
year = 1998}
|
|
131 |
|
|
132 |
@BOOK{Barendregt81,
|
|
133 |
AUTHOR = "H.~Barendregt",
|
|
134 |
TITLE = "{T}he {L}ambda {C}alculus: {I}ts {S}yntax and {S}emantics",
|
|
135 |
PUBLISHER = "North-Holland",
|
|
136 |
YEAR = 1981,
|
|
137 |
VOLUME = 103,
|
|
138 |
SERIES = "Studies in Logic and the Foundations of Mathematics"
|
|
139 |
}
|
|
140 |
|
|
141 |
@BOOK{CurryFeys58,
|
|
142 |
AUTHOR = "H.~B.~Curry and R.~Feys",
|
|
143 |
TITLE = "{C}ombinatory {L}ogic",
|
|
144 |
PUBLISHER = "North-Holland",
|
|
145 |
YEAR = "1958",
|
|
146 |
VOLUME = 1,
|
|
147 |
SERIES = "Studies in Logic and the Foundations of Mathematics"
|
|
148 |
}
|
|
149 |
|
|
150 |
@Unpublished{UrbanKaliszyk11,
|
|
151 |
author = {C.~Urban and C.~Kaliszyk},
|
|
152 |
title = {{G}eneral {B}indings and {A}lpha-{E}quivalence in {N}ominal {I}sabelle},
|
|
153 |
note = {submitted for publication},
|
|
154 |
month = {July},
|
|
155 |
year = {2010},
|
2237
|
156 |
}
|
|
157 |
|
|
158 |
@InProceedings{BengtsonParrow07,
|
|
159 |
author = {J.~Bengtson and J.~Parrow},
|
|
160 |
title = {Formalising the pi-{C}alculus using {N}ominal {L}ogic},
|
|
161 |
booktitle = {Proc.~of the 10th FOSSACS Conference},
|
|
162 |
year = 2007,
|
|
163 |
pages = {63--77},
|
|
164 |
series = {LNCS},
|
|
165 |
volume = {4423}
|
|
166 |
}
|
|
167 |
|
|
168 |
@inproceedings{BengtsonParow09,
|
|
169 |
author = {J.~Bengtson and J.~Parrow},
|
|
170 |
title = {{P}si-{C}alculi in {I}sabelle},
|
|
171 |
booktitle = {Proc of the 22nd TPHOLs Conference},
|
|
172 |
year = 2009,
|
|
173 |
pages = {99--114},
|
|
174 |
series = {LNCS},
|
|
175 |
volume = {5674}
|
|
176 |
}
|
|
177 |
|
|
178 |
@inproceedings{TobinHochstadtFelleisen08,
|
|
179 |
author = {S.~Tobin-Hochstadt and M.~Felleisen},
|
|
180 |
booktitle = {Proc.~of the 35rd POPL Symposium},
|
|
181 |
title = {{T}he {D}esign and {I}mplementation of {T}yped {S}cheme},
|
|
182 |
publisher = {ACM},
|
|
183 |
year = {2008},
|
|
184 |
pages = {395--406}
|
|
185 |
}
|
|
186 |
|
|
187 |
@InProceedings{UrbanCheneyBerghofer08,
|
|
188 |
author = "C.~Urban and J.~Cheney and S.~Berghofer",
|
|
189 |
title = "{M}echanizing the {M}etatheory of {LF}",
|
|
190 |
pages = "45--56",
|
|
191 |
year = 2008,
|
|
192 |
booktitle = "Proc.~of the 23rd LICS Symposium"
|
|
193 |
}
|
|
194 |
|
|
195 |
@InProceedings{UrbanZhu08,
|
|
196 |
title = "{R}evisiting {C}ut-{E}limination: {O}ne {D}ifficult {P}roof is {R}eally a {P}roof",
|
|
197 |
author = "C.~Urban and B.~Zhu",
|
|
198 |
booktitle = "Proc.~of the 9th RTA Conference",
|
|
199 |
year = "2008",
|
|
200 |
pages = "409--424",
|
|
201 |
series = "LNCS",
|
|
202 |
volume = 5117
|
2220
|
203 |
} |