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