neuper@48775
|
1 |
@Misc{coq-team-10,
|
neuper@48775
|
2 |
author = {Coq development team},
|
neuper@48775
|
3 |
title = {Coq 8.3 Reference Manual},
|
neuper@48775
|
4 |
howpublished = {http://coq.inria.fr/reman},
|
neuper@48775
|
5 |
year = {2010},
|
neuper@48775
|
6 |
note = {INRIA}
|
neuper@48775
|
7 |
}
|
neuper@48775
|
8 |
|
neuper@48771
|
9 |
@Book{db:dom-eng,
|
neuper@48771
|
10 |
author = {Bj{\o}rner, Dines},
|
neuper@48771
|
11 |
title = {Domain Engineering. Technology Management, Research and Engineering},
|
neuper@48771
|
12 |
publisher = {JAIST Press},
|
neuper@48771
|
13 |
year = {2009},
|
neuper@48771
|
14 |
month = {Feb},
|
neuper@48771
|
15 |
series = {COE Research Monograph Series},
|
neuper@48771
|
16 |
volume = {4},
|
neuper@48771
|
17 |
address = {Nomi, Japan}
|
neuper@48771
|
18 |
}
|
neuper@48771
|
19 |
|
neuper@48771
|
20 |
@INPROCEEDINGS{Hansen94b,
|
neuper@48771
|
21 |
KEY = "Hansen94",
|
neuper@48771
|
22 |
AUTHOR = "Kirsten Mark Hansen",
|
neuper@48771
|
23 |
EDITOR = "M. Naftalin, T. Denvir, M. Bertran",
|
neuper@48771
|
24 |
TITLE = "Validation of a Railway Interlocking Model",
|
neuper@48771
|
25 |
BOOKTITLE = "FME'94: Industrial Benefit of Formal Methods",
|
neuper@48771
|
26 |
PUBLISHER = "Springer-Verlag",
|
neuper@48771
|
27 |
YEAR = "1994",
|
neuper@48771
|
28 |
MONTH = "October",
|
neuper@48771
|
29 |
PAGES = "582-601",
|
neuper@48771
|
30 |
ANNOTE = "",
|
neuper@48771
|
31 |
COMMENT = "PGL has got the proceedings. ADN"
|
neuper@48771
|
32 |
}
|
neuper@48771
|
33 |
|
neuper@48771
|
34 |
@INPROCEEDINGS{Dehbonei&94,
|
neuper@48771
|
35 |
KEY = "Dehbonei\&94",
|
neuper@48771
|
36 |
AUTHOR = "Dehbonei, Babak and Mejia, Fernando",
|
neuper@48771
|
37 |
EDITOR = "M. Naftalin, T. Denvir, M. Bertran",
|
neuper@48771
|
38 |
TITLE = "Formal Methods in the Railways Signalling Industry",
|
neuper@48771
|
39 |
BOOKTITLE = "FME'94:Industrial Benefit of Formal Methods",
|
neuper@48771
|
40 |
PUBLISHER = "Springer-Verlag",
|
neuper@48771
|
41 |
YEAR = "1994",
|
neuper@48771
|
42 |
MONTH = "October",
|
neuper@48771
|
43 |
PAGES = "26-34",
|
neuper@48771
|
44 |
ANNOTE = "",
|
neuper@48771
|
45 |
COMMENT = "Peter has got the proceedings. ADN"
|
neuper@48771
|
46 |
}
|
neuper@48771
|
47 |
|
neuper@48771
|
48 |
@Book{db:SW-engIII,
|
neuper@48771
|
49 |
author = {Bj{\o}rner, Dines},
|
neuper@48771
|
50 |
title = {Software Engineering},
|
neuper@48771
|
51 |
publisher = {Springer},
|
neuper@48771
|
52 |
year = {2006},
|
neuper@48771
|
53 |
volume = {3},
|
neuper@48771
|
54 |
series = {Texts in Theoretical Computer Science},
|
neuper@48771
|
55 |
address = {Berlin, Heidelberg}
|
neuper@48771
|
56 |
}
|
neuper@48771
|
57 |
|
neuper@42504
|
58 |
@Book{pl:milner97,
|
neuper@42504
|
59 |
author = {Robin Milner and Mads Tofte and Robert Harper and David MacQueen},
|
neuper@42504
|
60 |
title = {The Definition of Standard ML (Revised)},
|
neuper@42504
|
61 |
publisher = {The MIT Press},
|
neuper@42504
|
62 |
year = 1997,
|
neuper@42504
|
63 |
address = {Cambridge, London},
|
neuper@42504
|
64 |
annote = {97bok375}
|
neuper@42504
|
65 |
}
|
neuper@42504
|
66 |
|
neuper@42503
|
67 |
@book{nipk:rew-all-that,
|
neuper@42503
|
68 |
title={Term rewriting and all that},
|
neuper@42503
|
69 |
author={Baader, Franz and Nipkow, Tobias },
|
neuper@42503
|
70 |
publisher={Cambridge University Press},year={1998},
|
neuper@42503
|
71 |
volume={},series={},address={},edition={},month={},
|
neuper@42503
|
72 |
note={},status={},source={},location={IST}
|
neuper@42503
|
73 |
}
|
neuper@42503
|
74 |
|
neuper@42498
|
75 |
@Misc{jrocnik-bakk,
|
neuper@42498
|
76 |
author = {Jan Rocnik},
|
neuper@42498
|
77 |
title = {Interactive Course Material for Signal Processing based on Isabelle/{\isac}},
|
neuper@42498
|
78 |
howpublished = {Bakkalaureate Thesis},
|
neuper@42498
|
79 |
year = {2012},
|
neuper@42498
|
80 |
note = {IST, Graz University of Technology, http://www.ist.tugraz.at/projects/isac/publ/jrocnik\_bakk.pdf}
|
neuper@42498
|
81 |
}
|
neuper@42498
|
82 |
|
jan@42463
|
83 |
@book{proakis2004contemporary,
|
jan@42463
|
84 |
title={Contemporary communication systems using MATLAB and Simulink},
|
jan@42463
|
85 |
author={Proakis, J.G. and Salehi, M. and Bauch, G.},
|
jan@42463
|
86 |
isbn={9780534406172},
|
jan@42463
|
87 |
lccn={31054410},
|
jan@42463
|
88 |
series={BookWare companion series},
|
jan@42463
|
89 |
url={http://books.google.at/books?id=5mXGQgAACAAJ},
|
jan@42463
|
90 |
year={2004},
|
jan@42463
|
91 |
publisher={Thomson--Brooks/Cole}
|
jan@42463
|
92 |
}
|
jan@42463
|
93 |
@book{oppenheim2010discrete,
|
jan@42463
|
94 |
title={Discrete-time signal processing},
|
jan@42463
|
95 |
author={Oppenheim, A.V. and Schafer, R.W.},
|
jan@42463
|
96 |
isbn={9780131988422},
|
jan@42463
|
97 |
series={Prentice-Hall signal processing series},
|
jan@42463
|
98 |
url={http://books.google.at/books?id=mYsoAQAAMAAJ},
|
jan@42463
|
99 |
year={2010},
|
jan@42463
|
100 |
publisher={Prentice Hall}
|
jan@42463
|
101 |
}
|
jan@42463
|
102 |
@manual{wenzel2011system,
|
jan@42463
|
103 |
title={The Isabelle System Manual},
|
jan@42463
|
104 |
author={Wenzel, M. and Berghofer, S.},
|
jan@42463
|
105 |
organization={TU Muenchen},
|
jan@42463
|
106 |
year={2011},
|
jan@42463
|
107 |
month={January}
|
jan@42463
|
108 |
}
|
jan@42463
|
109 |
@Book{Nipkow-Paulson-Wenzel:2002,
|
jan@42463
|
110 |
author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
|
jan@42463
|
111 |
title = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
|
jan@42463
|
112 |
publisher = {Springer},
|
jan@42463
|
113 |
series = {LNCS},
|
jan@42463
|
114 |
volume = 2283,
|
jan@42463
|
115 |
year = 2002}
|
jan@42463
|
116 |
@Book{progr-mathematica,
|
jan@42463
|
117 |
author = {Maeder, Roman E.},
|
jan@42463
|
118 |
title = {Programming in Mathematica},
|
jan@42463
|
119 |
publisher = {Addison-Wesley},
|
jan@42463
|
120 |
address = {Reading, Mass.},
|
jan@42463
|
121 |
year = {1997}
|
jan@42463
|
122 |
}
|
jan@42463
|
123 |
@Book{prog-maple06,
|
jan@42463
|
124 |
author = {Aladjav, Victor and Bogdevicius, Marijonas},
|
jan@42463
|
125 |
title = {Maple: Programming, Physical and Engineering Problems},
|
jan@42463
|
126 |
publisher = {Fultus Corporation},
|
jan@42463
|
127 |
year = {2006},
|
jan@42463
|
128 |
month = {February 27},
|
jan@42463
|
129 |
annote = {ISBN: 1596820802}
|
jan@42463
|
130 |
}
|
jan@42463
|
131 |
@Article{plmms10,
|
jan@42463
|
132 |
author = {Florian Haftmann and Cezary Kaliszyk and Walther Neuper},
|
jan@42463
|
133 |
title = {{CTP}-based programming languages~? Considerations about an experimental design},
|
jan@42463
|
134 |
journal = {ACM Communications in Computer Algebra},
|
jan@42463
|
135 |
year = {2010},
|
jan@42463
|
136 |
volume = {44},
|
jan@42463
|
137 |
number = {1/2},
|
jan@42463
|
138 |
pages = {27-41},
|
neuper@42468
|
139 |
month = {March/June}
|
jan@42463
|
140 |
}
|
jan@42463
|
141 |
@inproceedings{casproto,
|
jan@42463
|
142 |
author = {Cezary Kaliszyk and
|
jan@42463
|
143 |
Freek Wiedijk},
|
jan@42463
|
144 |
title = {Certified Computer Algebra on Top of an Interactive Theorem
|
jan@42463
|
145 |
Prover},
|
jan@42463
|
146 |
booktitle = {Calculemus},
|
jan@42463
|
147 |
year = {2007},
|
jan@42463
|
148 |
pages = {94-105},
|
jan@42463
|
149 |
ee = {http://dx.doi.org/10.1007/978-3-540-73086-6_8},
|
jan@42463
|
150 |
crossref = {DBLP:conf/mkm/2007},
|
jan@42463
|
151 |
bibsource = {DBLP, http://dblp.uni-trier.de}
|
jan@42463
|
152 |
}
|
jan@42463
|
153 |
@InProceedings{wn:lucas-interp-12,
|
jan@42463
|
154 |
author = {Neuper, Walther},
|
jan@42463
|
155 |
title = {Automated Generation of User Guidance by Combining Computation and Deduction},
|
jan@42463
|
156 |
booktitle = {THedu'11: CTP-compontents for educational software},
|
jan@42463
|
157 |
year = {2012},
|
jan@42463
|
158 |
editor = {Quaresma, Pedro},
|
jan@42463
|
159 |
publisher = {EPTCS},
|
jan@42463
|
160 |
note = {To appear}
|
jan@42463
|
161 |
}
|
jan@42463
|
162 |
@Manual{Huet_all:94,
|
jan@42463
|
163 |
author = {Huet, G. and Kahn, G. and Paulin-Mohring, C.},
|
jan@42463
|
164 |
title = {The Coq Proof Assistant},
|
jan@42463
|
165 |
institution = {INRIA-Rocquencourt},
|
jan@42463
|
166 |
year = {1994},
|
jan@42463
|
167 |
type = {Tutorial},
|
jan@42463
|
168 |
number = {Version 5.10},
|
jan@42463
|
169 |
address = {CNRS-ENS Lyon},
|
jan@42463
|
170 |
status={},source={Theorema},location={-}
|
jan@42463
|
171 |
}
|
jan@42463
|
172 |
@TECHREPORT{Back-SD09,
|
jan@42463
|
173 |
author = {Back, Ralph-Johan},
|
jan@42463
|
174 |
title = {Structured Derivations as a Unified Proof Style for Teaching Mathematics},
|
jan@42463
|
175 |
institution = {TUCS - Turku Centre for Computer Science},
|
jan@42463
|
176 |
year = {2009},
|
jan@42463
|
177 |
type = {TUCS Technical Report},
|
jan@42463
|
178 |
number = {949},
|
jan@42463
|
179 |
address = {Turku, Finland},
|
jan@42463
|
180 |
month = {July}
|
jan@42463
|
181 |
}
|
jan@42463
|
182 |
@InProceedings{ActiveMath-MAIN11,
|
neuper@42468
|
183 |
author = {Melis, Erica and Siekmann, Jörg},
|
jan@42463
|
184 |
title = {An Intelligent Tutoring System for Mathematics},
|
jan@42463
|
185 |
booktitle = {Seventh International Conference Artificial Intelligence and Soft Computing (ICAISC)},
|
jan@42463
|
186 |
pages = {91-101},
|
jan@42463
|
187 |
year = {2004},
|
jan@42463
|
188 |
editor = {Rutkowski, L. and Siekmann, J. and Tadeusiewicz, R. and Zadeh, L.A.},
|
jan@42463
|
189 |
number = {3070,},
|
jan@42463
|
190 |
series = {LNAI},
|
jan@42463
|
191 |
publisher = {Springer-Verlag},
|
jan@42463
|
192 |
doi = {doi:10.1007/978-3-540-24844-6\_12}}
|
jan@42463
|
193 |
@TechReport{mat-tutor-cmu-MAIN11,
|
jan@42463
|
194 |
author = {John R. Anderson},
|
jan@42463
|
195 |
title = {Intelligent Tutoring and High School Mathematics},
|
jan@42463
|
196 |
institution = {Carnegie Mellon University, Department of Psychology},
|
jan@42463
|
197 |
year = {2008},
|
jan@42463
|
198 |
type = {Technical Report},
|
jan@42463
|
199 |
number = {20},
|
jan@42463
|
200 |
note = {http://repository.cmu.edu/psychology/20}
|
jan@42463
|
201 |
}
|
jan@42463
|
202 |
@PhdThesis{proof-strategies-11,
|
jan@42463
|
203 |
author = {Dietrich, Dominik},
|
jan@42463
|
204 |
title = {Proof Planning with Compiled Strategies},
|
jan@42463
|
205 |
school = {FR 6.2 Informatik, Saarland University},
|
jan@42463
|
206 |
year = {2011}
|
jan@42463
|
207 |
}
|
jan@42463
|
208 |
@proceedings{DBLP:conf/mkm/2007,
|
jan@42463
|
209 |
editor = {Manuel Kauers and
|
jan@42463
|
210 |
Manfred Kerber and
|
jan@42463
|
211 |
Robert Miner and
|
jan@42463
|
212 |
Wolfgang Windsteiger},
|
jan@42463
|
213 |
title = {Towards Mechanized Mathematical Assistants, 14th Symposium,
|
jan@42463
|
214 |
Calculemus 2007, 6th International Conference, MKM 2007,
|
jan@42463
|
215 |
Hagenberg, Austria, June 27-30, 2007, Proceedings},
|
jan@42463
|
216 |
booktitle = {Calculemus/MKM},
|
jan@42463
|
217 |
publisher = {Springer},
|
jan@42463
|
218 |
series = {Lecture Notes in Computer Science},
|
jan@42463
|
219 |
volume = {4573},
|
jan@42463
|
220 |
year = {2007},
|
jan@42463
|
221 |
isbn = {978-3-540-73083-5},
|
jan@42463
|
222 |
bibsource = {DBLP, http://dblp.uni-trier.de}
|
jan@42463
|
223 |
}
|
neuper@42464
|
224 |
|
neuper@42464
|
225 |
@InProceedings{gdaroczy-EP-13,
|
neuper@42464
|
226 |
author = {Gabriella Dar\'{o}czy and Walther Neuper},
|
jan@42473
|
227 |
booktitle = {unknown},
|
neuper@42507
|
228 |
title = {Error-Patterns within ``Next-Step-Guidance'' in TP-based Educational Systems},
|
neuper@42464
|
229 |
OPTpages = {TODO-TODO},
|
neuper@42507
|
230 |
crossref = {eduTPS-12},
|
neuper@42507
|
231 |
note = {to appear in this publication}
|
neuper@42464
|
232 |
}
|
neuper@42464
|
233 |
|
neuper@42464
|
234 |
|
neuper@42464
|
235 |
@Proceedings{eduTPS-12,
|
neuper@42464
|
236 |
title = {Theorem-Prover based Systems for Education (eduTPS)},
|
neuper@42464
|
237 |
year = {2013},
|
neuper@42464
|
238 |
OPTkey = {},
|
neuper@42464
|
239 |
OPTbooktitle = {},
|
neuper@42464
|
240 |
OPTeditor = {},
|
neuper@42464
|
241 |
OPTvolume = {},
|
neuper@42464
|
242 |
OPTnumber = {},
|
neuper@42464
|
243 |
OPTseries = {},
|
neuper@42464
|
244 |
OPTaddress = {},
|
neuper@42464
|
245 |
OPTmonth = {},
|
neuper@42464
|
246 |
OPTorganization = {},
|
neuper@42464
|
247 |
publisher = {The Electronic Journal of Mathematics and Technology},
|
neuper@42464
|
248 |
note = {to appear},
|
neuper@42464
|
249 |
OPTannote = {}
|
neuper@42464
|
250 |
}
|
neuper@42464
|
251 |
|
neuper@42464
|
252 |
@Misc{nipkow-prog-prove,
|
neuper@42464
|
253 |
author = {Nipkow, Tobias},
|
neuper@42464
|
254 |
title = {Programming and Proving in {Isabelle/HOL}},
|
neuper@42464
|
255 |
howpublished = {contained in the Isabelle distribution},
|
neuper@42464
|
256 |
month = {May 22},
|
neuper@42464
|
257 |
year = {2012}
|
neuper@42464
|
258 |
}
|
neuper@42464
|
259 |
|
neuper@42464
|
260 |
@Book{pl:hind97,
|
neuper@42464
|
261 |
author = {J. Roger Hindley},
|
neuper@42464
|
262 |
title = {Basic Simple Type Theory},
|
neuper@42464
|
263 |
publisher = {Cambridge University Press},
|
neuper@42464
|
264 |
year = 1997,
|
neuper@42464
|
265 |
editor = {S. Abramsky and P. H. Aczel and others},
|
neuper@42464
|
266 |
number = 42,
|
neuper@42464
|
267 |
series = {Cambridge Tracts in Theoretical Computer Science},
|
neuper@42464
|
268 |
address = {Cambridge},
|
neuper@42464
|
269 |
annote = {97bok308}
|
neuper@42464
|
270 |
}
|
neuper@42464
|
271 |
|
neuper@42464
|
272 |
@Article{Milner-78,
|
neuper@42464
|
273 |
author = {Milner, R.},
|
neuper@42464
|
274 |
title = {A Theory of Type Polymorphism in Programming},
|
neuper@42464
|
275 |
journal = {Journal of Computer and System Science (JCSS)},
|
neuper@42464
|
276 |
year = {1978},
|
neuper@42464
|
277 |
number = {17},
|
jan@42473
|
278 |
volume = {0},
|
neuper@42464
|
279 |
pages = {348-374}
|
neuper@42464
|
280 |
}
|
neuper@42465
|
281 |
|
neuper@42465
|
282 |
@inproceedings{Wenzel-11:doc-orient,
|
neuper@42465
|
283 |
author = {Wenzel, Makarius},
|
neuper@42465
|
284 |
title = {Isabelle as document-oriented proof assistant},
|
neuper@42465
|
285 |
booktitle = {Proceedings of the 18th Calculemus and 10th international conference on Intelligent computer mathematics},
|
neuper@42465
|
286 |
series = {MKM'11},
|
neuper@42465
|
287 |
year = {2011},
|
neuper@42465
|
288 |
isbn = {978-3-642-22672-4},
|
neuper@42465
|
289 |
location = {Bertinoro, Italy},
|
neuper@42465
|
290 |
pages = {244--259},
|
neuper@42465
|
291 |
numpages = {16},
|
neuper@42465
|
292 |
url = {http://dl.acm.org/citation.cfm?id=2032713.2032732},
|
neuper@42465
|
293 |
acmid = {2032732},
|
neuper@42465
|
294 |
publisher = {Springer-Verlag},
|
neuper@42465
|
295 |
address = {Berlin, Heidelberg},
|
neuper@42465
|
296 |
}
|
neuper@42468
|
297 |
@InProceedings{makar-jedit-12,
|
neuper@42468
|
298 |
author = {Makarius Wenzel},
|
neuper@42468
|
299 |
title = {Isabelle/{jEdit} — a Prover IDE within the {PIDE} framework},
|
neuper@42468
|
300 |
booktitle = {Conference on Intelligent Computer Mathematics (CICM 2012)},
|
neuper@42468
|
301 |
year = {2012},
|
neuper@42468
|
302 |
editor = { J. Jeuring and others},
|
neuper@42468
|
303 |
number = {7362},
|
neuper@42468
|
304 |
series = {LNAI},
|
neuper@42468
|
305 |
publisher = {Springer}
|
neuper@42468
|
306 |
}
|
neuper@42465
|
307 |
|
neuper@42465
|
308 |
@InProceedings{Makarius-09:parall-proof,
|
neuper@42465
|
309 |
author = {Wenzel, Makarius},
|
neuper@42465
|
310 |
title = {Parallel Proof Checking in {Isabelle/Isar}},
|
neuper@42465
|
311 |
booktitle = {ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS)},
|
neuper@42465
|
312 |
year = {2009},
|
neuper@42465
|
313 |
editor = {Dos Reis and L. Th\'ery},
|
neuper@42465
|
314 |
address = {Munich},
|
neuper@42465
|
315 |
month = {August},
|
neuper@42465
|
316 |
publisher = {ACM Digital library}
|
neuper@42465
|
317 |
}
|
neuper@42478
|
318 |
|
neuper@42478
|
319 |
@Book{fm-03,
|
neuper@42478
|
320 |
author = {Jean Francois Monin and Michael G. Hinchey},
|
neuper@42478
|
321 |
title = {Understanding formal methods},
|
neuper@42478
|
322 |
publisher = {Springer},
|
neuper@42478
|
323 |
year = {2003}
|
neuper@42478
|
324 |
}
|
neuper@42478
|
325 |
|
jan@48774
|
326 |
@misc{wiki:1,
|
jan@48767
|
327 |
author = {Wikipedia},
|
jan@48767
|
328 |
Title = {Table of common Z-transform pairs},
|
jan@48767
|
329 |
year = {2012},
|
jan@48767
|
330 |
url = {http://en.wikipedia.org/wiki/Z-transform#Table_of_common_Z-transform_pairs},
|
jan@48767
|
331 |
note = {[Online; accessed 31-Oct-2012]}
|
neuper@48771
|
332 |
}
|
neuper@48771
|
333 |
|
neuper@48771
|
334 |
@InProceedings{kremp.np:assess,
|
neuper@48771
|
335 |
author = {Krempler, Alan and Neuper, Walther},
|
neuper@48771
|
336 |
title = {Formative Assessment for User Guidance in Single Stepping Systems},
|
neuper@48771
|
337 |
booktitle = {Interactive Computer Aided Learning, Proceedings of ICL08},
|
neuper@48771
|
338 |
year = {2008},
|
neuper@48771
|
339 |
editor = {Aucher, Michael E.},
|
jan@48774
|
340 |
address = {Villach, Austria},
|
jan@48774
|
341 |
note = {$\,$\\http://www.ist.tugraz.at/projects/isac/publ/icl08.pdf}
|
neuper@48771
|
342 |
}
|
neuper@48771
|
343 |
|