2 author = {Coq development team},
3 title = {Coq 8.3 Reference Manual},
4 howpublished = {http://coq.inria.fr/reman},
10 author = {Bj{\o}rner, Dines},
11 title = {Domain Engineering. Technology Management, Research and Engineering},
12 publisher = {JAIST Press},
15 series = {COE Research Monograph Series},
17 address = {Nomi, Japan}
20 @INPROCEEDINGS{Hansen94b,
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",
31 COMMENT = "PGL has got the proceedings. ADN"
34 @INPROCEEDINGS{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",
45 COMMENT = "Peter has got the proceedings. ADN"
49 author = {Bj{\o}rner, Dines},
50 title = {Software Engineering},
51 publisher = {Springer},
54 series = {Texts in Theoretical Computer Science},
55 address = {Berlin, Heidelberg}
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},
63 address = {Cambridge, London},
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}
76 author = {Jan Rocnik},
77 title = {Interactive Course Material for Signal Processing based on Isabelle/{\isac}},
78 howpublished = {Bakkalaureate Thesis},
80 note = {IST, Graz University of Technology, http://www.ist.tugraz.at/projects/isac/publ/jrocnik\_bakk.pdf}
83 @book{proakis2004contemporary,
84 title={Contemporary communication systems using MATLAB and Simulink},
85 author={Proakis, J.G. and Salehi, M. and Bauch, G.},
88 series={BookWare companion series},
89 url={http://books.google.at/books?id=5mXGQgAACAAJ},
91 publisher={Thomson--Brooks/Cole}
93 @book{oppenheim2010discrete,
94 title={Discrete-time signal processing},
95 author={Oppenheim, A.V. and Schafer, R.W.},
97 series={Prentice-Hall signal processing series},
98 url={http://books.google.at/books?id=mYsoAQAAMAAJ},
100 publisher={Prentice Hall}
102 @manual{wenzel2011system,
103 title={The Isabelle System Manual},
104 author={Wenzel, M. and Berghofer, S.},
105 organization={TU Muenchen},
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},
116 @Book{progr-mathematica,
117 author = {Maeder, Roman E.},
118 title = {Programming in Mathematica},
119 publisher = {Addison-Wesley},
120 address = {Reading, Mass.},
124 author = {Aladjav, Victor and Bogdevicius, Marijonas},
125 title = {Maple: Programming, Physical and Engineering Problems},
126 publisher = {Fultus Corporation},
128 month = {February 27},
129 annote = {ISBN: 1596820802}
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},
141 @inproceedings{casproto,
142 author = {Cezary Kaliszyk and
144 title = {Certified Computer Algebra on Top of an Interactive Theorem
146 booktitle = {Calculemus},
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}
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},
158 editor = {Quaresma, Pedro},
163 author = {Huet, G. and Kahn, G. and Paulin-Mohring, C.},
164 title = {The Coq Proof Assistant},
165 institution = {INRIA-Rocquencourt},
168 number = {Version 5.10},
169 address = {CNRS-ENS Lyon},
170 status={},source={Theorema},location={-}
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},
177 type = {TUCS Technical Report},
179 address = {Turku, Finland},
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)},
188 editor = {Rutkowski, L. and Siekmann, J. and Tadeusiewicz, R. and Zadeh, L.A.},
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},
198 type = {Technical Report},
200 note = {http://repository.cmu.edu/psychology/20}
202 @PhdThesis{proof-strategies-11,
203 author = {Dietrich, Dominik},
204 title = {Proof Planning with Compiled Strategies},
205 school = {FR 6.2 Informatik, Saarland University},
208 @proceedings{DBLP:conf/mkm/2007,
209 editor = {Manuel Kauers 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},
221 isbn = {978-3-540-73083-5},
222 bibsource = {DBLP, http://dblp.uni-trier.de}
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}
235 @Proceedings{eduTPS-12,
236 title = {Theorem-Prover based Systems for Education (eduTPS)},
246 OPTorganization = {},
247 publisher = {The Electronic Journal of Mathematics and Technology},
252 @Misc{nipkow-prog-prove,
253 author = {Nipkow, Tobias},
254 title = {Programming and Proving in {Isabelle/HOL}},
255 howpublished = {contained in the Isabelle distribution},
261 author = {J. Roger Hindley},
262 title = {Basic Simple Type Theory},
263 publisher = {Cambridge University Press},
265 editor = {S. Abramsky and P. H. Aczel and others},
267 series = {Cambridge Tracts in Theoretical Computer Science},
268 address = {Cambridge},
273 author = {Milner, R.},
274 title = {A Theory of Type Polymorphism in Programming},
275 journal = {Journal of Computer and System Science (JCSS)},
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},
288 isbn = {978-3-642-22672-4},
289 location = {Bertinoro, Italy},
292 url = {http://dl.acm.org/citation.cfm?id=2032713.2032732},
294 publisher = {Springer-Verlag},
295 address = {Berlin, Heidelberg},
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)},
302 editor = { J. Jeuring and others},
305 publisher = {Springer}
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)},
313 editor = {Dos Reis and L. Th\'ery},
316 publisher = {ACM Digital library}
320 author = {Jean Francois Monin and Michael G. Hinchey},
321 title = {Understanding formal methods},
322 publisher = {Springer},
327 author = {Bj{\o}rner, Dines},
328 title = {Domain Engineering. Technology Management, Research and Engineering},
329 publisher = {JAIST Press},
332 series = {COE Research Monograph Series},
334 address = {Nomi, Japan}
338 author = {Wikipedia},
339 Title = {Table of common Z-transform pairs},
341 url = {http://en.wikipedia.org/wiki/Z-transform#Table_of_common_Z-transform_pairs},
342 note = {[Online; accessed 31-Oct-2012]}
345 @InProceedings{kremp.np:assess,
346 author = {Krempler, Alan and Neuper, Walther},
347 title = {Formative Assessment for User Guidance in Single Stepping Systems},
348 booktitle = {Interactive Computer Aided Learning, Proceedings of ICL08},
350 editor = {Aucher, Michael E.},
351 address = {Villach, Austria} %,
352 %note = {$\,$\\http://www.ist.tugraz.at/projects/isac/publ/icl08.pdf}