diff -r 7f3760f39bdc -r f8845fc8f38d src/Doc/isac/jrocnik/eJMT-paper/references.bib --- a/src/Doc/isac/jrocnik/eJMT-paper/references.bib Mon Sep 16 12:27:20 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,343 +0,0 @@ -@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} -} -