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