biblio.bib 9.25 KB
Newer Older
Dennis Müller's avatar
Dennis Müller committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149

@online{wikipedia:matroid,
  label = {MWP},
  title = {Matroid --- Wikipedia{,} The Free Encyclopedia},
  urldate = {2018-04-4},
  url = {https://en.wikipedia.org/w/index.php?title=Matroid}}
@Article{imps,
  author =	"W. Farmer and J. Guttman and F. Thayer",
  title =	"{IMPS: An Interactive Mathematical Proof System}",
  journal =	"{Journal of Automated Reasoning}",
  pages =	"213--248",
  volume =	"11",
  number =	"2",
  year = 	"1993",
}
@Book{isabelle,
  author =	"L. Paulson",
  title =	"{Isabelle: A Generic Theorem Prover}",
  publisher =	"Springer",
  series =	"Lecture Notes in Computer Science",
  volume =	"828",
  year = 	"1994",
}
@INPROCEEDINGS{NorKoh:efnrsmk07,
  author = {Immanuel Normann and Michael Kohlhase},
  title = {Extended Formula Normalization for $\epsilon$-Retrieval and
           Sharing of Mathematical Knowledge},
  pages = {266--279},
  crossref = {MKM07},
  keywords = {conference},
 pubs = {mkohlhase,mws,omdoc}}
@inproceedings{KMOR:pvs:17,
  author = "M. Kohlhase and D. M{\"u}ller and S. Owre and F. Rabe",
  title = "{Making PVS Accessible to Generic Services by Interpretation in a Universal Format}",
  year = "2017",
  pages = "319--335",
  booktitle = "Interactive Theorem Proving",
  editor = "M. Ayala-Rincon and C. Munoz",
  publisher = "Springer"
}
@inproceedings{hol_isahol_matching,
  author = {T. Gauthier and C. Kaliszyk},
  title = "{Matching concepts across HOL libraries}",
  booktitle = {Intelligent Computer Mathematics},
  editor = {S. Watt and J. Davenport and A. Sexton and P. Sojka and J. Urban},
  pages = {267--281},
  year = 2014,
  publisher = {Springer}
}
@online{OAFproject:on,
  label = {OAF},
  url = {https://kwarc.info/projects/oaf/},
  title = {{OAF}: An Open Archive for Formalizations},
  urldate = {2018-04-26}}
@Article{lf,
  author = 	 "R. Harper and F. Honsell and G. Plotkin",
  title = 	 "{A framework for defining logics}",
  journal =	 "{Journal of the Association for Computing Machinery}",
  year =	 1993,
  volume =	 40,
  number = 	1,
  pages =	 "143--184",
}
@inproceedings{KKMR:alignments:16,
  author = "C. Kaliszyk and M. Kohlhase and D. M{\"u}ller and F. Rabe",
  title = "{A Standard for Aligning Mathematical Concepts}",
  year = "2016",
  pages = "229--244",
  booktitle = "Work in Progress at CICM 2016",
  editor = "A. Kohlhase and M. Kohlhase and P. Libbrecht and B. Miller and F. Tompa and A. Naummowicz and W. Neuper and P. Quaresma and M. Suda",
  publisher = "CEUR-WS.org"
}
@inproceedings{ODK:mitm:16,
  author = "P. Dehaye and M. Iancu and M. Kohlhase and A. Konovalov and S. Leli{\`e}vre and D. M{\"u}ller and M. Pfeiffer and F. Rabe and N. Thi{\'e}ry and T. Wiesing",
  title = "{Interoperability in the ODK Project: The Math-in-the-Middle Approach}",
  year = "2016",
  pages = "117--131",
  booktitle = "Intelligent Computer Mathematics",
  editor = "M. Kohlhase and L. {de Moura} and M. Johansson and B. Miller and F. Tompa",
  publisher = "Springer"
}
@inproceedings{MRLR:alignments:17,
  author = "D. M{\"u}ller and C. Rothgang and Y. Liu and F. Rabe",
  title = "{Alignment-based Translations Across Formal Systems Using Interface Theories}",
  year = "2017",
  pages = "77--93",
  booktitle = "Proof eXchange for Theorem Proving",
  editor = "C. Dubois and B. {Woltzenlogel Paleo}",
  publisher = "Open Publishing Association"
}
@INPROCEEDINGS{mathhub,
  author = "M. Iancu and C. Jucovschi and M. Kohlhase and T. Wiesing",
  title = "{System Description: MathHub.info}",
  booktitle = "Intelligent Computer Mathematics",
  editor = "S. Watt and J. Davenport and A. Sexton and P. Sojka and J. Urban",
  pages = "431--434",
  publisher = "Springer",
  year = {2014},
}
@inproceedings{RupKohMue:fitgv17,
  author = {Marcel Rupprecht and Michael Kohlhase and Dennis M{\"u}ller},
  title = {A Flexible, Interactive Theory-Graph Viewer},
  crossref = {MathUI17},
  url = {http://kwarc.info/kohlhase/papers/mathui17-tgview.pdf},
  pubs = {dmueller,mkohlhase,mrupprecht,odk,mathhub,odkWP6}}

@book{omdoc,
  author = "M. Kohlhase",
  title = "{OMDoc: An Open Markup Format for Mathematical Documents (Version 1.2)}",
  series = "{Lecture Notes in Artificial Intelligence}",
  number = "4180",
  publisher = "Springer",
  year = "2006",
}
@PROCEEDINGS{MKM07,
  title = {{MKM/Calculemus}},
  booktitle = {Towards Mechanized Mathematical Assistants. {MKM/Calculemus}},
  year = {2007},
  isbn = {978-3-540-73083-5},
  editor = {Manuel Kauers and Manfred Kerber and Robert Miner and Wolfgang Windsteiger},
  number = {4573},
  series = {LNAI},
  keywords = {conference},
  publisher = {Springer Verlag}}
@Proceedings{MathUI17,
  editor =   {Andrea Kohlhase and Marco Pollanen},
  title =    {MathUI 2017: The 12th Workshop on Mathematical User Interfaces},
  booktitle =    {MathUI 2017: The 12th Workshop on Mathematical User Interfaces},
  SOONurl = {http://ceur-ws.org/Vol-1785/},
  pubs = {akohlhase},
  year =    {2017}}

@article{RK:mmt:10,
  author = "F. Rabe and M. Kohlhase",
  title = "{A Scalable Module System}",
  year = "2013",
  pages = "1--54",
  journal = "Information and Computation",
  volume = "230",
  number = "1"
}
@inproceedings{KR:hollight:14,
  author = "C. Kaliszyk and F. Rabe",
  title = "{Towards Knowledge Management for HOL Light}",
  year = "2014",
  pages = "357--372",
  booktitle = "Intelligent Computer Mathematics",
  editor = "S. Watt and J. Davenport and A. Sexton and P. Sojka and J. Urban",
  publisher = "Springer"
Dennis Müller's avatar
update    
Dennis Müller committed
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
}

@Article{imps,
  author =	"W. Farmer and J. Guttman and F. Thayer",
  title =	"{IMPS: An Interactive Mathematical Proof System}",
  journal =	"{Journal of Automated Reasoning}",
  pages =	"213--248",
  volume =	"11",
  number =	"2",
  year = 	"1993",
}
@article{RK:mmt:10,
  author = "F. Rabe and M. Kohlhase",
  title = "{A Scalable Module System}",
  year = "2013",
  pages = "1--54",
  journal = "Information and Computation",
  volume = "230",
  number = "1"
}
@book{omdoc,
  author = "M. Kohlhase",
  title = "{OMDoc: An Open Markup Format for Mathematical Documents (Version 1.2)}",
  series = "{Lecture Notes in Artificial Intelligence}",
  number = "4180",
  publisher = "Springer",
  year = "2006",
}
@inproceedings{KMOR:pvs:17,
  author = "M. Kohlhase and D. M{\"u}ller and S. Owre and F. Rabe",
  title = "{Making PVS Accessible to Generic Services by Interpretation in a Universal Format}",
  year = "2017",
  pages = "319--335",
  booktitle = "Interactive Theorem Proving",
  editor = "M. Ayala-Rincon and C. Munoz",
  publisher = "Springer"
}
@inproceedings{KR:hollight:14,
  author = "C. Kaliszyk and F. Rabe",
  title = "{Towards Knowledge Management for HOL Light}",
  year = "2014",
  pages = "357--372",
  booktitle = "Intelligent Computer Mathematics",
  editor = "S. Watt and J. Davenport and A. Sexton and P. Sojka and J. Urban",
  publisher = "Springer"
}
@inproceedings{hol_isahol_matching,
  author = {T. Gauthier and C. Kaliszyk},
  title = "{Matching concepts across HOL libraries}",
  booktitle = {Intelligent Computer Mathematics},
  editor = {S. Watt and J. Davenport and A. Sexton and P. Sojka and J. Urban},
  pages = {267--281},
  year = 2014,
  publisher = {Springer}
}
@Article{lf,
  author = 	 "R. Harper and F. Honsell and G. Plotkin",
  title = 	 "{A framework for defining logics}",
  journal =	 "{Journal of the Association for Computing Machinery}",
  year =	 1993,
  volume =	 40,
  number = 	1,
  pages =	 "143--184",
}

@inproceedings{pvs,
    AUTHOR = {S. Owre and J. Rushby and N. Shankar},
    TITLE = "{PVS: A Prototype Verification System}",
    BOOKTITLE = "{11th International Conference on Automated Deduction (CADE)}",
    YEAR = {1992},
    EDITOR = {D. Kapur},
    PAGES = {748--752},
    PUBLISHER = {Springer},
}
Michael Kohlhase's avatar
Michael Kohlhase committed
224
225
226
@online{PVSlibraries:on,crossref={PVSlibraries:base},
  urldate = {2014-12-17},
  label = {PVS}}
Dennis Müller's avatar
update    
Dennis Müller committed
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
@MISC{PVSlibraries:url,crossref={PVSlibraries:base},key = {PVS},
  howpublished = {\url{http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/}}}
@MISC{PVSlibraries:base,
  title = {{NASA} {PVS} Library},
  url = {http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/}}
@BOOK{Graf:ti96,
  title = {Term Indexing},
  publisher = {Springer Verlag},
  year = {1996},
  author = {Graf, Peter},
  number = {1053},
  series = {LNCS}}
@inproceedings{am:doceng10,crossref={DOCENG10},
  author    = {Serge Autexier and Normen M{\"u}ller},
  title     = {Semantics-based Change Impact Analysis for Heterogeneous Collections of Documents},
  pages     = {97--106},
  numpages  = {10},
  url       = {http://doi.acm.org/10.1145/1860559.1860580},
  doi       = {http://doi.acm.org/10.1145/1860559.1860580},
  acmid     = {1860580},
  keywords  = {change impact analysis, document collections, document management, graph rewriting, semantics},
  pubs      = {nmueller,omoc,omdoc}}
@mastersthesis{iancu:msc,
  author = "Mihnea Iancu",
  title = "{Management of Change in Declarative Languages}",
  year = "2012",
  school = "Jacobs University Bremen",
  pubs={mscthesis}
}
@proceedings{DOCENG10,
  editor    = {Michael Gormish and Rolf Ingold},
  title = {Proceedings of the 10\textsuperscript{th} {ACM} symposium on Document engineering},
  booktitle = {Proceedings of the 10\textsuperscript{th} {ACM} symposium on Document engineering},
  series    = {DocEng '10},
  year      = {2010},
  isbn      = {978-1-4503-0231-9},
  location  = {Manchester, United Kingdom},
  publisher = {ACM},
  keywords = {conference},
Michael Kohlhase's avatar
Michael Kohlhase committed
266
  address   = {New York, NY, USA}}