1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-isac/jrocnik/eJMT-paper/references.bib Tue Sep 17 09:50:52 2013 +0200
1.3 @@ -0,0 +1,343 @@
1.4 +@Misc{coq-team-10,
1.5 + author = {Coq development team},
1.6 + title = {Coq 8.3 Reference Manual},
1.7 + howpublished = {http://coq.inria.fr/reman},
1.8 + year = {2010},
1.9 + note = {INRIA}
1.10 +}
1.11 +
1.12 +@Book{db:dom-eng,
1.13 + author = {Bj{\o}rner, Dines},
1.14 + title = {Domain Engineering. Technology Management, Research and Engineering},
1.15 + publisher = {JAIST Press},
1.16 + year = {2009},
1.17 + month = {Feb},
1.18 + series = {COE Research Monograph Series},
1.19 + volume = {4},
1.20 + address = {Nomi, Japan}
1.21 +}
1.22 +
1.23 +@INPROCEEDINGS{Hansen94b,
1.24 + KEY = "Hansen94",
1.25 + AUTHOR = "Kirsten Mark Hansen",
1.26 + EDITOR = "M. Naftalin, T. Denvir, M. Bertran",
1.27 + TITLE = "Validation of a Railway Interlocking Model",
1.28 + BOOKTITLE = "FME'94: Industrial Benefit of Formal Methods",
1.29 + PUBLISHER = "Springer-Verlag",
1.30 + YEAR = "1994",
1.31 + MONTH = "October",
1.32 + PAGES = "582-601",
1.33 + ANNOTE = "",
1.34 + COMMENT = "PGL has got the proceedings. ADN"
1.35 +}
1.36 +
1.37 +@INPROCEEDINGS{Dehbonei&94,
1.38 + KEY = "Dehbonei\&94",
1.39 + AUTHOR = "Dehbonei, Babak and Mejia, Fernando",
1.40 + EDITOR = "M. Naftalin, T. Denvir, M. Bertran",
1.41 + TITLE = "Formal Methods in the Railways Signalling Industry",
1.42 + BOOKTITLE = "FME'94:Industrial Benefit of Formal Methods",
1.43 + PUBLISHER = "Springer-Verlag",
1.44 + YEAR = "1994",
1.45 + MONTH = "October",
1.46 + PAGES = "26-34",
1.47 + ANNOTE = "",
1.48 + COMMENT = "Peter has got the proceedings. ADN"
1.49 +}
1.50 +
1.51 +@Book{db:SW-engIII,
1.52 + author = {Bj{\o}rner, Dines},
1.53 + title = {Software Engineering},
1.54 + publisher = {Springer},
1.55 + year = {2006},
1.56 + volume = {3},
1.57 + series = {Texts in Theoretical Computer Science},
1.58 + address = {Berlin, Heidelberg}
1.59 +}
1.60 +
1.61 +@Book{pl:milner97,
1.62 + author = {Robin Milner and Mads Tofte and Robert Harper and David MacQueen},
1.63 + title = {The Definition of Standard ML (Revised)},
1.64 + publisher = {The MIT Press},
1.65 + year = 1997,
1.66 + address = {Cambridge, London},
1.67 + annote = {97bok375}
1.68 +}
1.69 +
1.70 +@book{nipk:rew-all-that,
1.71 + title={Term rewriting and all that},
1.72 + author={Baader, Franz and Nipkow, Tobias },
1.73 + publisher={Cambridge University Press},year={1998},
1.74 + volume={},series={},address={},edition={},month={},
1.75 + note={},status={},source={},location={IST}
1.76 + }
1.77 +
1.78 +@Misc{jrocnik-bakk,
1.79 + author = {Jan Rocnik},
1.80 + title = {Interactive Course Material for Signal Processing based on Isabelle/{\isac}},
1.81 + howpublished = {Bakkalaureate Thesis},
1.82 + year = {2012},
1.83 + note = {IST, Graz University of Technology, http://www.ist.tugraz.at/projects/isac/publ/jrocnik\_bakk.pdf}
1.84 +}
1.85 +
1.86 +@book{proakis2004contemporary,
1.87 + title={Contemporary communication systems using MATLAB and Simulink},
1.88 + author={Proakis, J.G. and Salehi, M. and Bauch, G.},
1.89 + isbn={9780534406172},
1.90 + lccn={31054410},
1.91 + series={BookWare companion series},
1.92 + url={http://books.google.at/books?id=5mXGQgAACAAJ},
1.93 + year={2004},
1.94 + publisher={Thomson--Brooks/Cole}
1.95 +}
1.96 +@book{oppenheim2010discrete,
1.97 + title={Discrete-time signal processing},
1.98 + author={Oppenheim, A.V. and Schafer, R.W.},
1.99 + isbn={9780131988422},
1.100 + series={Prentice-Hall signal processing series},
1.101 + url={http://books.google.at/books?id=mYsoAQAAMAAJ},
1.102 + year={2010},
1.103 + publisher={Prentice Hall}
1.104 +}
1.105 +@manual{wenzel2011system,
1.106 + title={The Isabelle System Manual},
1.107 + author={Wenzel, M. and Berghofer, S.},
1.108 + organization={TU Muenchen},
1.109 + year={2011},
1.110 + month={January}
1.111 +}
1.112 +@Book{Nipkow-Paulson-Wenzel:2002,
1.113 + author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
1.114 + title = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
1.115 + publisher = {Springer},
1.116 + series = {LNCS},
1.117 + volume = 2283,
1.118 + year = 2002}
1.119 +@Book{progr-mathematica,
1.120 + author = {Maeder, Roman E.},
1.121 + title = {Programming in Mathematica},
1.122 + publisher = {Addison-Wesley},
1.123 + address = {Reading, Mass.},
1.124 + year = {1997}
1.125 +}
1.126 +@Book{prog-maple06,
1.127 + author = {Aladjav, Victor and Bogdevicius, Marijonas},
1.128 + title = {Maple: Programming, Physical and Engineering Problems},
1.129 + publisher = {Fultus Corporation},
1.130 + year = {2006},
1.131 + month = {February 27},
1.132 + annote = {ISBN: 1596820802}
1.133 +}
1.134 +@Article{plmms10,
1.135 + author = {Florian Haftmann and Cezary Kaliszyk and Walther Neuper},
1.136 + title = {{CTP}-based programming languages~? Considerations about an experimental design},
1.137 + journal = {ACM Communications in Computer Algebra},
1.138 + year = {2010},
1.139 + volume = {44},
1.140 + number = {1/2},
1.141 + pages = {27-41},
1.142 + month = {March/June}
1.143 +}
1.144 +@inproceedings{casproto,
1.145 + author = {Cezary Kaliszyk and
1.146 + Freek Wiedijk},
1.147 + title = {Certified Computer Algebra on Top of an Interactive Theorem
1.148 + Prover},
1.149 + booktitle = {Calculemus},
1.150 + year = {2007},
1.151 + pages = {94-105},
1.152 + ee = {http://dx.doi.org/10.1007/978-3-540-73086-6_8},
1.153 + crossref = {DBLP:conf/mkm/2007},
1.154 + bibsource = {DBLP, http://dblp.uni-trier.de}
1.155 +}
1.156 +@InProceedings{wn:lucas-interp-12,
1.157 + author = {Neuper, Walther},
1.158 + title = {Automated Generation of User Guidance by Combining Computation and Deduction},
1.159 + booktitle = {THedu'11: CTP-compontents for educational software},
1.160 + year = {2012},
1.161 + editor = {Quaresma, Pedro},
1.162 + publisher = {EPTCS},
1.163 + note = {To appear}
1.164 +}
1.165 +@Manual{Huet_all:94,
1.166 + author = {Huet, G. and Kahn, G. and Paulin-Mohring, C.},
1.167 + title = {The Coq Proof Assistant},
1.168 + institution = {INRIA-Rocquencourt},
1.169 + year = {1994},
1.170 + type = {Tutorial},
1.171 + number = {Version 5.10},
1.172 + address = {CNRS-ENS Lyon},
1.173 + status={},source={Theorema},location={-}
1.174 +}
1.175 +@TECHREPORT{Back-SD09,
1.176 + author = {Back, Ralph-Johan},
1.177 + title = {Structured Derivations as a Unified Proof Style for Teaching Mathematics},
1.178 + institution = {TUCS - Turku Centre for Computer Science},
1.179 + year = {2009},
1.180 + type = {TUCS Technical Report},
1.181 + number = {949},
1.182 + address = {Turku, Finland},
1.183 + month = {July}
1.184 +}
1.185 +@InProceedings{ActiveMath-MAIN11,
1.186 + author = {Melis, Erica and Siekmann, Jörg},
1.187 + title = {An Intelligent Tutoring System for Mathematics},
1.188 + booktitle = {Seventh International Conference Artificial Intelligence and Soft Computing (ICAISC)},
1.189 + pages = {91-101},
1.190 + year = {2004},
1.191 + editor = {Rutkowski, L. and Siekmann, J. and Tadeusiewicz, R. and Zadeh, L.A.},
1.192 + number = {3070,},
1.193 + series = {LNAI},
1.194 + publisher = {Springer-Verlag},
1.195 + doi = {doi:10.1007/978-3-540-24844-6\_12}}
1.196 +@TechReport{mat-tutor-cmu-MAIN11,
1.197 + author = {John R. Anderson},
1.198 + title = {Intelligent Tutoring and High School Mathematics},
1.199 + institution = {Carnegie Mellon University, Department of Psychology},
1.200 + year = {2008},
1.201 + type = {Technical Report},
1.202 + number = {20},
1.203 + note = {http://repository.cmu.edu/psychology/20}
1.204 +}
1.205 +@PhdThesis{proof-strategies-11,
1.206 + author = {Dietrich, Dominik},
1.207 + title = {Proof Planning with Compiled Strategies},
1.208 + school = {FR 6.2 Informatik, Saarland University},
1.209 + year = {2011}
1.210 +}
1.211 +@proceedings{DBLP:conf/mkm/2007,
1.212 + editor = {Manuel Kauers and
1.213 + Manfred Kerber and
1.214 + Robert Miner and
1.215 + Wolfgang Windsteiger},
1.216 + title = {Towards Mechanized Mathematical Assistants, 14th Symposium,
1.217 + Calculemus 2007, 6th International Conference, MKM 2007,
1.218 + Hagenberg, Austria, June 27-30, 2007, Proceedings},
1.219 + booktitle = {Calculemus/MKM},
1.220 + publisher = {Springer},
1.221 + series = {Lecture Notes in Computer Science},
1.222 + volume = {4573},
1.223 + year = {2007},
1.224 + isbn = {978-3-540-73083-5},
1.225 + bibsource = {DBLP, http://dblp.uni-trier.de}
1.226 +}
1.227 +
1.228 +@InProceedings{gdaroczy-EP-13,
1.229 + author = {Gabriella Dar\'{o}czy and Walther Neuper},
1.230 + booktitle = {unknown},
1.231 + title = {Error-Patterns within ``Next-Step-Guidance'' in TP-based Educational Systems},
1.232 + OPTpages = {TODO-TODO},
1.233 + crossref = {eduTPS-12},
1.234 + note = {to appear in this publication}
1.235 +}
1.236 +
1.237 +
1.238 +@Proceedings{eduTPS-12,
1.239 + title = {Theorem-Prover based Systems for Education (eduTPS)},
1.240 + year = {2013},
1.241 + OPTkey = {},
1.242 + OPTbooktitle = {},
1.243 + OPTeditor = {},
1.244 + OPTvolume = {},
1.245 + OPTnumber = {},
1.246 + OPTseries = {},
1.247 + OPTaddress = {},
1.248 + OPTmonth = {},
1.249 + OPTorganization = {},
1.250 + publisher = {The Electronic Journal of Mathematics and Technology},
1.251 + note = {to appear},
1.252 + OPTannote = {}
1.253 +}
1.254 +
1.255 +@Misc{nipkow-prog-prove,
1.256 + author = {Nipkow, Tobias},
1.257 + title = {Programming and Proving in {Isabelle/HOL}},
1.258 + howpublished = {contained in the Isabelle distribution},
1.259 + month = {May 22},
1.260 + year = {2012}
1.261 +}
1.262 +
1.263 +@Book{pl:hind97,
1.264 + author = {J. Roger Hindley},
1.265 + title = {Basic Simple Type Theory},
1.266 + publisher = {Cambridge University Press},
1.267 + year = 1997,
1.268 + editor = {S. Abramsky and P. H. Aczel and others},
1.269 + number = 42,
1.270 + series = {Cambridge Tracts in Theoretical Computer Science},
1.271 + address = {Cambridge},
1.272 + annote = {97bok308}
1.273 +}
1.274 +
1.275 +@Article{Milner-78,
1.276 + author = {Milner, R.},
1.277 + title = {A Theory of Type Polymorphism in Programming},
1.278 + journal = {Journal of Computer and System Science (JCSS)},
1.279 + year = {1978},
1.280 + number = {17},
1.281 + volume = {0},
1.282 + pages = {348-374}
1.283 +}
1.284 +
1.285 +@inproceedings{Wenzel-11:doc-orient,
1.286 + author = {Wenzel, Makarius},
1.287 + title = {Isabelle as document-oriented proof assistant},
1.288 + booktitle = {Proceedings of the 18th Calculemus and 10th international conference on Intelligent computer mathematics},
1.289 + series = {MKM'11},
1.290 + year = {2011},
1.291 + isbn = {978-3-642-22672-4},
1.292 + location = {Bertinoro, Italy},
1.293 + pages = {244--259},
1.294 + numpages = {16},
1.295 + url = {http://dl.acm.org/citation.cfm?id=2032713.2032732},
1.296 + acmid = {2032732},
1.297 + publisher = {Springer-Verlag},
1.298 + address = {Berlin, Heidelberg},
1.299 +}
1.300 +@InProceedings{makar-jedit-12,
1.301 + author = {Makarius Wenzel},
1.302 + title = {Isabelle/{jEdit} — a Prover IDE within the {PIDE} framework},
1.303 + booktitle = {Conference on Intelligent Computer Mathematics (CICM 2012)},
1.304 + year = {2012},
1.305 + editor = { J. Jeuring and others},
1.306 + number = {7362},
1.307 + series = {LNAI},
1.308 + publisher = {Springer}
1.309 +}
1.310 +
1.311 +@InProceedings{Makarius-09:parall-proof,
1.312 + author = {Wenzel, Makarius},
1.313 + title = {Parallel Proof Checking in {Isabelle/Isar}},
1.314 + booktitle = {ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS)},
1.315 + year = {2009},
1.316 + editor = {Dos Reis and L. Th\'ery},
1.317 + address = {Munich},
1.318 + month = {August},
1.319 + publisher = {ACM Digital library}
1.320 +}
1.321 +
1.322 +@Book{fm-03,
1.323 + author = {Jean Francois Monin and Michael G. Hinchey},
1.324 + title = {Understanding formal methods},
1.325 + publisher = {Springer},
1.326 + year = {2003}
1.327 +}
1.328 +
1.329 +@misc{wiki:1,
1.330 + author = {Wikipedia},
1.331 + Title = {Table of common Z-transform pairs},
1.332 + year = {2012},
1.333 + url = {http://en.wikipedia.org/wiki/Z-transform#Table_of_common_Z-transform_pairs},
1.334 + note = {[Online; accessed 31-Oct-2012]}
1.335 + }
1.336 +
1.337 +@InProceedings{kremp.np:assess,
1.338 + author = {Krempler, Alan and Neuper, Walther},
1.339 + title = {Formative Assessment for User Guidance in Single Stepping Systems},
1.340 + booktitle = {Interactive Computer Aided Learning, Proceedings of ICL08},
1.341 + year = {2008},
1.342 + editor = {Aucher, Michael E.},
1.343 + address = {Villach, Austria},
1.344 + note = {$\,$\\http://www.ist.tugraz.at/projects/isac/publ/icl08.pdf}
1.345 +}
1.346 +