3 title = {Interactive Course Material for Signal Processing based on Isabelle/{\isac}},
4 howpublished = {Bakkalaureate Thesis},
6 note = {IST, Graz University of Technology, http://www.ist.tugraz.at/projects/isac/publ/jrocnik\_bakk.pdf}
9 @book{proakis2004contemporary,
10 title={Contemporary communication systems using MATLAB and Simulink},
11 author={Proakis, J.G. and Salehi, M. and Bauch, G.},
14 series={BookWare companion series},
15 url={http://books.google.at/books?id=5mXGQgAACAAJ},
17 publisher={Thomson--Brooks/Cole}
19 @book{oppenheim2010discrete,
20 title={Discrete-time signal processing},
21 author={Oppenheim, A.V. and Schafer, R.W.},
23 series={Prentice-Hall signal processing series},
24 url={http://books.google.at/books?id=mYsoAQAAMAAJ},
26 publisher={Prentice Hall}
28 @manual{wenzel2011system,
29 title={The Isabelle System Manual},
30 author={Wenzel, M. and Berghofer, S.},
31 organization={TU Muenchen},
35 @Book{Nipkow-Paulson-Wenzel:2002,
36 author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
37 title = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
38 publisher = {Springer},
42 @Book{progr-mathematica,
43 author = {Maeder, Roman E.},
44 title = {Programming in Mathematica},
45 publisher = {Addison-Wesley},
46 address = {Reading, Mass.},
50 author = {Aladjav, Victor and Bogdevicius, Marijonas},
51 title = {Maple: Programming, Physical and Engineering Problems},
52 publisher = {Fultus Corporation},
54 month = {February 27},
55 annote = {ISBN: 1596820802}
58 author = {Florian Haftmann and Cezary Kaliszyk and Walther Neuper},
59 title = {{CTP}-based programming languages~? Considerations about an experimental design},
60 journal = {ACM Communications in Computer Algebra},
67 @inproceedings{casproto,
68 author = {Cezary Kaliszyk and
70 title = {Certified Computer Algebra on Top of an Interactive Theorem
72 booktitle = {Calculemus},
75 ee = {http://dx.doi.org/10.1007/978-3-540-73086-6_8},
76 crossref = {DBLP:conf/mkm/2007},
77 bibsource = {DBLP, http://dblp.uni-trier.de}
79 @InProceedings{wn:lucas-interp-12,
80 author = {Neuper, Walther},
81 title = {Automated Generation of User Guidance by Combining Computation and Deduction},
82 booktitle = {THedu'11: CTP-compontents for educational software},
84 editor = {Quaresma, Pedro},
89 author = {Huet, G. and Kahn, G. and Paulin-Mohring, C.},
90 title = {The Coq Proof Assistant},
91 institution = {INRIA-Rocquencourt},
94 number = {Version 5.10},
95 address = {CNRS-ENS Lyon},
96 status={},source={Theorema},location={-}
98 @TECHREPORT{Back-SD09,
99 author = {Back, Ralph-Johan},
100 title = {Structured Derivations as a Unified Proof Style for Teaching Mathematics},
101 institution = {TUCS - Turku Centre for Computer Science},
103 type = {TUCS Technical Report},
105 address = {Turku, Finland},
108 @InProceedings{ActiveMath-MAIN11,
109 author = {Melis, Erica and Siekmann, Jörg},
110 title = {An Intelligent Tutoring System for Mathematics},
111 booktitle = {Seventh International Conference Artificial Intelligence and Soft Computing (ICAISC)},
114 editor = {Rutkowski, L. and Siekmann, J. and Tadeusiewicz, R. and Zadeh, L.A.},
117 publisher = {Springer-Verlag},
118 doi = {doi:10.1007/978-3-540-24844-6\_12}}
119 @TechReport{mat-tutor-cmu-MAIN11,
120 author = {John R. Anderson},
121 title = {Intelligent Tutoring and High School Mathematics},
122 institution = {Carnegie Mellon University, Department of Psychology},
124 type = {Technical Report},
126 note = {http://repository.cmu.edu/psychology/20}
128 @PhdThesis{proof-strategies-11,
129 author = {Dietrich, Dominik},
130 title = {Proof Planning with Compiled Strategies},
131 school = {FR 6.2 Informatik, Saarland University},
134 @proceedings{DBLP:conf/mkm/2007,
135 editor = {Manuel Kauers and
138 Wolfgang Windsteiger},
139 title = {Towards Mechanized Mathematical Assistants, 14th Symposium,
140 Calculemus 2007, 6th International Conference, MKM 2007,
141 Hagenberg, Austria, June 27-30, 2007, Proceedings},
142 booktitle = {Calculemus/MKM},
143 publisher = {Springer},
144 series = {Lecture Notes in Computer Science},
147 isbn = {978-3-540-73083-5},
148 bibsource = {DBLP, http://dblp.uni-trier.de}
151 @InProceedings{gdaroczy-EP-13,
152 author = {Gabriella Dar\'{o}czy and Walther Neuper},
153 booktitle = {unknown},
154 title = {Exploitation of ``Next-Step-Guidance'' in a {TP}-based Math Assistant},
155 OPTpages = {TODO-TODO},
156 crossref = {eduTPS-12}
160 @Proceedings{eduTPS-12,
161 title = {Theorem-Prover based Systems for Education (eduTPS)},
171 OPTorganization = {},
172 publisher = {The Electronic Journal of Mathematics and Technology},
177 @Misc{nipkow-prog-prove,
178 author = {Nipkow, Tobias},
179 title = {Programming and Proving in {Isabelle/HOL}},
180 howpublished = {contained in the Isabelle distribution},
186 author = {J. Roger Hindley},
187 title = {Basic Simple Type Theory},
188 publisher = {Cambridge University Press},
190 editor = {S. Abramsky and P. H. Aczel and others},
192 series = {Cambridge Tracts in Theoretical Computer Science},
193 address = {Cambridge},
198 author = {Milner, R.},
199 title = {A Theory of Type Polymorphism in Programming},
200 journal = {Journal of Computer and System Science (JCSS)},
207 @inproceedings{Wenzel-11:doc-orient,
208 author = {Wenzel, Makarius},
209 title = {Isabelle as document-oriented proof assistant},
210 booktitle = {Proceedings of the 18th Calculemus and 10th international conference on Intelligent computer mathematics},
213 isbn = {978-3-642-22672-4},
214 location = {Bertinoro, Italy},
217 url = {http://dl.acm.org/citation.cfm?id=2032713.2032732},
219 publisher = {Springer-Verlag},
220 address = {Berlin, Heidelberg},
222 @InProceedings{makar-jedit-12,
223 author = {Makarius Wenzel},
224 title = {Isabelle/{jEdit} — a Prover IDE within the {PIDE} framework},
225 booktitle = {Conference on Intelligent Computer Mathematics (CICM 2012)},
227 editor = { J. Jeuring and others},
230 publisher = {Springer}
233 @InProceedings{Makarius-09:parall-proof,
234 author = {Wenzel, Makarius},
235 title = {Parallel Proof Checking in {Isabelle/Isar}},
236 booktitle = {ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS)},
238 editor = {Dos Reis and L. Th\'ery},
241 publisher = {ACM Digital library}
245 author = {Jean Francois Monin and Michael G. Hinchey},
246 title = {Understanding formal methods},
247 publisher = {Springer},
252 author = {Bj{\o}rner, Dines},
253 title = {Domain Engineering. Technology Management, Research and Engineering},
254 publisher = {JAIST Press},
257 series = {COE Research Monograph Series},
259 address = {Nomi, Japan}