35 |
35 |
36 @inproceedings{ChicliPS02, |
36 @inproceedings{ChicliPS02, |
37 author = {Laurent Chicli and |
37 author = {Laurent Chicli and |
38 Loic Pottier and |
38 Loic Pottier and |
39 Carlos Simpson}, |
39 Carlos Simpson}, |
40 title = {Mathematical Quotients and Quotient Types in Coq}, |
40 title = {{M}athematical {Q}uotients and {Q}uotient {T}ypes in {C}oq}, |
41 booktitle = {TYPES}, |
41 booktitle = {TYPES}, |
42 year = {2002}, |
42 year = {2002}, |
43 pages = {95-107}, |
43 pages = {95-107}, |
44 ee = {http://link.springer.de/link/service/series/0558/bibs/2646/26460095.htm}, |
44 ee = {http://link.springer.de/link/service/series/0558/bibs/2646/26460095.htm}, |
45 crossref = {DBLP:conf/types/2002}, |
45 crossref = {DBLP:conf/types/2002}, |
127 @BOOK{harrison-thesis, |
127 @BOOK{harrison-thesis, |
128 author = "John Harrison", |
128 author = "John Harrison", |
129 title = "Theorem Proving with the Real Numbers", |
129 title = "Theorem Proving with the Real Numbers", |
130 publisher = "Springer-Verlag", |
130 publisher = "Springer-Verlag", |
131 year = 1998} |
131 year = 1998} |
|
132 |
|
133 @BOOK{Barendregt81, |
|
134 AUTHOR = "H.~Barendregt", |
|
135 TITLE = "{T}he {L}ambda {C}alculus: {I}ts {S}yntax and {S}emantics", |
|
136 PUBLISHER = "North-Holland", |
|
137 YEAR = 1981, |
|
138 VOLUME = 103, |
|
139 SERIES = "Studies in Logic and the Foundations of Mathematics" |
|
140 } |
|
141 |
|
142 @BOOK{CurryFeys58, |
|
143 AUTHOR = "H.~B.~Curry and R.~Feys", |
|
144 TITLE = "{C}ombinatory {L}ogic", |
|
145 PUBLISHER = "North-Holland", |
|
146 YEAR = "1958", |
|
147 VOLUME = 1, |
|
148 SERIES = "Studies in Logic and the Foundations of Mathematics" |
|
149 } |
|
150 |
|
151 @Unpublished{UrbanKaliszyk11, |
|
152 author = {C.~Urban and C.~Kaliszyk}, |
|
153 title = {{G}eneral {B}indings and {A}lpha-{E}quivalence in {N}ominal {I}sabelle}, |
|
154 note = {submitted for publication}, |
|
155 month = {July}, |
|
156 year = {2010}, |
|
157 } |
|
158 |
|
159 @InProceedings{BengtsonParrow07, |
|
160 author = {J.~Bengtson and J.~Parrow}, |
|
161 title = {Formalising the pi-{C}alculus using {N}ominal {L}ogic}, |
|
162 booktitle = {Proc.~of the 10th FOSSACS Conference}, |
|
163 year = 2007, |
|
164 pages = {63--77}, |
|
165 series = {LNCS}, |
|
166 volume = {4423} |
|
167 } |
|
168 |
|
169 @inproceedings{BengtsonParow09, |
|
170 author = {J.~Bengtson and J.~Parrow}, |
|
171 title = {{P}si-{C}alculi in {I}sabelle}, |
|
172 booktitle = {Proc of the 22nd TPHOLs Conference}, |
|
173 year = 2009, |
|
174 pages = {99--114}, |
|
175 series = {LNCS}, |
|
176 volume = {5674} |
|
177 } |
|
178 |
|
179 @inproceedings{TobinHochstadtFelleisen08, |
|
180 author = {S.~Tobin-Hochstadt and M.~Felleisen}, |
|
181 booktitle = {Proc.~of the 35rd POPL Symposium}, |
|
182 title = {{T}he {D}esign and {I}mplementation of {T}yped {S}cheme}, |
|
183 publisher = {ACM}, |
|
184 year = {2008}, |
|
185 pages = {395--406} |
|
186 } |
|
187 |
|
188 @InProceedings{UrbanCheneyBerghofer08, |
|
189 author = "C.~Urban and J.~Cheney and S.~Berghofer", |
|
190 title = "{M}echanizing the {M}etatheory of {LF}", |
|
191 pages = "45--56", |
|
192 year = 2008, |
|
193 booktitle = "Proc.~of the 23rd LICS Symposium" |
|
194 } |
|
195 |
|
196 @InProceedings{UrbanZhu08, |
|
197 title = "{R}evisiting {C}ut-{E}limination: {O}ne {D}ifficult {P}roof is {R}eally a {P}roof", |
|
198 author = "C.~Urban and B.~Zhu", |
|
199 booktitle = "Proc.~of the 9th RTA Conference", |
|
200 year = "2008", |
|
201 pages = "409--424", |
|
202 series = "LNCS", |
|
203 volume = 5117 |
|
204 } |