@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}

}