1 @inproceedings{Nogin02, |
|
2 author = {Aleksey Nogin}, |
|
3 title = {Quotient Types: A Modular Approach}, |
|
4 booktitle = {Proc.~of the 15th TPHOLs conference}, |
|
5 year = {2002}, |
|
6 pages = {263-280}, |
|
7 series = {LNCS}, |
|
8 volume = {2646} |
|
9 } |
|
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= {{T}heory {I}nterpretations 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 = {{M}athematical {Q}uotients and {Q}uotient {T}ypes in {C}oq}, |
|
41 booktitle = {Proc of the TYPES workshop}, |
|
42 year = {2002}, |
|
43 pages = {95-107}, |
|
44 series = {LNCS}, |
|
45 volume = {2646} |
|
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}, |
|
79 booktitle = {Proc.~of the 10th TPHOLs conference}, |
|
80 year = {1997}, |
|
81 pages = {291-306}, |
|
82 series = {LNCS}, |
|
83 volume = {1275} |
|
84 } |
|
85 |
|
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}, |
|
104 booktitle = {Proc of the 18th TPHOLs conference}, |
|
105 year = {2005}, |
|
106 pages = {130-146}, |
|
107 series = {LNCS}, |
|
108 volume = {3603} |
|
109 } |
|
110 |
|
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", |
|
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}, |
|
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 |
|
203 } |
|