diff -r 7f3760f39bdc -r f8845fc8f38d doc-isac/jrocnik/eJMT-paper/references.bib --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-isac/jrocnik/eJMT-paper/references.bib Tue Sep 17 09:50:52 2013 +0200 @@ -0,0 +1,343 @@ +@Misc{coq-team-10, + author = {Coq development team}, + title = {Coq 8.3 Reference Manual}, + howpublished = {http://coq.inria.fr/reman}, + year = {2010}, + note = {INRIA} +} + +@Book{db:dom-eng, + author = {Bj{\o}rner, Dines}, + title = {Domain Engineering. Technology Management, Research and Engineering}, + publisher = {JAIST Press}, + year = {2009}, + month = {Feb}, + series = {COE Research Monograph Series}, + volume = {4}, + address = {Nomi, Japan} +} + +@INPROCEEDINGS{Hansen94b, + KEY = "Hansen94", + AUTHOR = "Kirsten Mark Hansen", + EDITOR = "M. Naftalin, T. Denvir, M. Bertran", + TITLE = "Validation of a Railway Interlocking Model", + BOOKTITLE = "FME'94: Industrial Benefit of Formal Methods", + PUBLISHER = "Springer-Verlag", + YEAR = "1994", + MONTH = "October", + PAGES = "582-601", + ANNOTE = "", + COMMENT = "PGL has got the proceedings. ADN" +} + +@INPROCEEDINGS{Dehbonei&94, + KEY = "Dehbonei\&94", + AUTHOR = "Dehbonei, Babak and Mejia, Fernando", + EDITOR = "M. Naftalin, T. Denvir, M. Bertran", + TITLE = "Formal Methods in the Railways Signalling Industry", + BOOKTITLE = "FME'94:Industrial Benefit of Formal Methods", + PUBLISHER = "Springer-Verlag", + YEAR = "1994", + MONTH = "October", + PAGES = "26-34", + ANNOTE = "", + COMMENT = "Peter has got the proceedings. ADN" +} + +@Book{db:SW-engIII, + author = {Bj{\o}rner, Dines}, + title = {Software Engineering}, + publisher = {Springer}, + year = {2006}, + volume = {3}, + series = {Texts in Theoretical Computer Science}, + address = {Berlin, Heidelberg} +} + +@Book{pl:milner97, + author = {Robin Milner and Mads Tofte and Robert Harper and David MacQueen}, + title = {The Definition of Standard ML (Revised)}, + publisher = {The MIT Press}, + year = 1997, + address = {Cambridge, London}, + annote = {97bok375} +} + +@book{nipk:rew-all-that, + title={Term rewriting and all that}, + author={Baader, Franz and Nipkow, Tobias }, + publisher={Cambridge University Press},year={1998}, + volume={},series={},address={},edition={},month={}, + note={},status={},source={},location={IST} + } + +@Misc{jrocnik-bakk, + author = {Jan Rocnik}, + title = {Interactive Course Material for Signal Processing based on Isabelle/{\isac}}, + howpublished = {Bakkalaureate Thesis}, + year = {2012}, + note = {IST, Graz University of Technology, http://www.ist.tugraz.at/projects/isac/publ/jrocnik\_bakk.pdf} +} + +@book{proakis2004contemporary, + title={Contemporary communication systems using MATLAB and Simulink}, + author={Proakis, J.G. and Salehi, M. and Bauch, G.}, + isbn={9780534406172}, + lccn={31054410}, + series={BookWare companion series}, + url={http://books.google.at/books?id=5mXGQgAACAAJ}, + year={2004}, + publisher={Thomson--Brooks/Cole} +} +@book{oppenheim2010discrete, + title={Discrete-time signal processing}, + author={Oppenheim, A.V. and Schafer, R.W.}, + isbn={9780131988422}, + series={Prentice-Hall signal processing series}, + url={http://books.google.at/books?id=mYsoAQAAMAAJ}, + year={2010}, + publisher={Prentice Hall} +} +@manual{wenzel2011system, + title={The Isabelle System Manual}, + author={Wenzel, M. and Berghofer, S.}, + organization={TU Muenchen}, + year={2011}, + month={January} +} +@Book{Nipkow-Paulson-Wenzel:2002, + author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, + title = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic}, + publisher = {Springer}, + series = {LNCS}, + volume = 2283, + year = 2002} +@Book{progr-mathematica, + author = {Maeder, Roman E.}, + title = {Programming in Mathematica}, + publisher = {Addison-Wesley}, + address = {Reading, Mass.}, + year = {1997} +} +@Book{prog-maple06, + author = {Aladjav, Victor and Bogdevicius, Marijonas}, + title = {Maple: Programming, Physical and Engineering Problems}, + publisher = {Fultus Corporation}, + year = {2006}, + month = {February 27}, + annote = {ISBN: 1596820802} +} +@Article{plmms10, + author = {Florian Haftmann and Cezary Kaliszyk and Walther Neuper}, + title = {{CTP}-based programming languages~? Considerations about an experimental design}, + journal = {ACM Communications in Computer Algebra}, + year = {2010}, + volume = {44}, + number = {1/2}, + pages = {27-41}, + month = {March/June} +} +@inproceedings{casproto, + author = {Cezary Kaliszyk and + Freek Wiedijk}, + title = {Certified Computer Algebra on Top of an Interactive Theorem + Prover}, + booktitle = {Calculemus}, + year = {2007}, + pages = {94-105}, + ee = {http://dx.doi.org/10.1007/978-3-540-73086-6_8}, + crossref = {DBLP:conf/mkm/2007}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} +@InProceedings{wn:lucas-interp-12, + author = {Neuper, Walther}, + title = {Automated Generation of User Guidance by Combining Computation and Deduction}, + booktitle = {THedu'11: CTP-compontents for educational software}, + year = {2012}, + editor = {Quaresma, Pedro}, + publisher = {EPTCS}, + note = {To appear} +} +@Manual{Huet_all:94, + author = {Huet, G. and Kahn, G. and Paulin-Mohring, C.}, + title = {The Coq Proof Assistant}, + institution = {INRIA-Rocquencourt}, + year = {1994}, + type = {Tutorial}, + number = {Version 5.10}, + address = {CNRS-ENS Lyon}, + status={},source={Theorema},location={-} +} +@TECHREPORT{Back-SD09, + author = {Back, Ralph-Johan}, + title = {Structured Derivations as a Unified Proof Style for Teaching Mathematics}, + institution = {TUCS - Turku Centre for Computer Science}, + year = {2009}, + type = {TUCS Technical Report}, + number = {949}, + address = {Turku, Finland}, + month = {July} +} +@InProceedings{ActiveMath-MAIN11, + author = {Melis, Erica and Siekmann, Jörg}, + title = {An Intelligent Tutoring System for Mathematics}, + booktitle = {Seventh International Conference Artificial Intelligence and Soft Computing (ICAISC)}, + pages = {91-101}, + year = {2004}, + editor = {Rutkowski, L. and Siekmann, J. and Tadeusiewicz, R. and Zadeh, L.A.}, + number = {3070,}, + series = {LNAI}, + publisher = {Springer-Verlag}, + doi = {doi:10.1007/978-3-540-24844-6\_12}} +@TechReport{mat-tutor-cmu-MAIN11, + author = {John R. Anderson}, + title = {Intelligent Tutoring and High School Mathematics}, + institution = {Carnegie Mellon University, Department of Psychology}, + year = {2008}, + type = {Technical Report}, + number = {20}, + note = {http://repository.cmu.edu/psychology/20} +} +@PhdThesis{proof-strategies-11, + author = {Dietrich, Dominik}, + title = {Proof Planning with Compiled Strategies}, + school = {FR 6.2 Informatik, Saarland University}, + year = {2011} +} +@proceedings{DBLP:conf/mkm/2007, + editor = {Manuel Kauers and + Manfred Kerber and + Robert Miner and + Wolfgang Windsteiger}, + title = {Towards Mechanized Mathematical Assistants, 14th Symposium, + Calculemus 2007, 6th International Conference, MKM 2007, + Hagenberg, Austria, June 27-30, 2007, Proceedings}, + booktitle = {Calculemus/MKM}, + publisher = {Springer}, + series = {Lecture Notes in Computer Science}, + volume = {4573}, + year = {2007}, + isbn = {978-3-540-73083-5}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} + +@InProceedings{gdaroczy-EP-13, + author = {Gabriella Dar\'{o}czy and Walther Neuper}, + booktitle = {unknown}, + title = {Error-Patterns within ``Next-Step-Guidance'' in TP-based Educational Systems}, + OPTpages = {TODO-TODO}, + crossref = {eduTPS-12}, + note = {to appear in this publication} +} + + +@Proceedings{eduTPS-12, + title = {Theorem-Prover based Systems for Education (eduTPS)}, + year = {2013}, + OPTkey = {}, + OPTbooktitle = {}, + OPTeditor = {}, + OPTvolume = {}, + OPTnumber = {}, + OPTseries = {}, + OPTaddress = {}, + OPTmonth = {}, + OPTorganization = {}, + publisher = {The Electronic Journal of Mathematics and Technology}, + note = {to appear}, + OPTannote = {} +} + +@Misc{nipkow-prog-prove, + author = {Nipkow, Tobias}, + title = {Programming and Proving in {Isabelle/HOL}}, + howpublished = {contained in the Isabelle distribution}, + month = {May 22}, + year = {2012} +} + +@Book{pl:hind97, + author = {J. Roger Hindley}, + title = {Basic Simple Type Theory}, + publisher = {Cambridge University Press}, + year = 1997, + editor = {S. Abramsky and P. H. Aczel and others}, + number = 42, + series = {Cambridge Tracts in Theoretical Computer Science}, + address = {Cambridge}, + annote = {97bok308} +} + +@Article{Milner-78, + author = {Milner, R.}, + title = {A Theory of Type Polymorphism in Programming}, + journal = {Journal of Computer and System Science (JCSS)}, + year = {1978}, + number = {17}, + volume = {0}, + pages = {348-374} +} + +@inproceedings{Wenzel-11:doc-orient, + author = {Wenzel, Makarius}, + title = {Isabelle as document-oriented proof assistant}, + booktitle = {Proceedings of the 18th Calculemus and 10th international conference on Intelligent computer mathematics}, + series = {MKM'11}, + year = {2011}, + isbn = {978-3-642-22672-4}, + location = {Bertinoro, Italy}, + pages = {244--259}, + numpages = {16}, + url = {http://dl.acm.org/citation.cfm?id=2032713.2032732}, + acmid = {2032732}, + publisher = {Springer-Verlag}, + address = {Berlin, Heidelberg}, +} +@InProceedings{makar-jedit-12, + author = {Makarius Wenzel}, + title = {Isabelle/{jEdit} — a Prover IDE within the {PIDE} framework}, + booktitle = {Conference on Intelligent Computer Mathematics (CICM 2012)}, + year = {2012}, + editor = { J. Jeuring and others}, + number = {7362}, + series = {LNAI}, + publisher = {Springer} +} + +@InProceedings{Makarius-09:parall-proof, + author = {Wenzel, Makarius}, + title = {Parallel Proof Checking in {Isabelle/Isar}}, + booktitle = {ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS)}, + year = {2009}, + editor = {Dos Reis and L. Th\'ery}, + address = {Munich}, + month = {August}, + publisher = {ACM Digital library} +} + +@Book{fm-03, + author = {Jean Francois Monin and Michael G. Hinchey}, + title = {Understanding formal methods}, + publisher = {Springer}, + year = {2003} +} + +@misc{wiki:1, + author = {Wikipedia}, + Title = {Table of common Z-transform pairs}, + year = {2012}, + url = {http://en.wikipedia.org/wiki/Z-transform#Table_of_common_Z-transform_pairs}, + note = {[Online; accessed 31-Oct-2012]} + } + +@InProceedings{kremp.np:assess, + author = {Krempler, Alan and Neuper, Walther}, + title = {Formative Assessment for User Guidance in Single Stepping Systems}, + booktitle = {Interactive Computer Aided Learning, Proceedings of ICL08}, + year = {2008}, + editor = {Aucher, Michael E.}, + address = {Villach, Austria}, + note = {$\,$\\http://www.ist.tugraz.at/projects/isac/publ/icl08.pdf} +} +