@book(prog-maple06,
 author       = "Victor Aladjav and Marijonas Bogdevicius",
 year         = "2006",
 title        = "Maple: Programming, Physical and Engineering Problems",
 publisher    = "Fultus Corporation",
)
@techreport(Back-SD09,
 author       = "Ralph-Johan Back",
 year         = "2009",
 title        = "Structured Derivations as a Unified Proof Style for Teaching Mathematics",
 type         = "TUCS Technical Report",
 number       = "949",
 institution  = "TUCS - Turku Centre for Computer Science",
 address      = "Turku, Finland",
)
@book(Back1998,
 author       = "Ralph-Johan Back and Joakim von Wright",
 year         = "1998",
 title        = "Refinement Calculus: A Systematic Introduction",
 publisher    = "Springer-Verlag",
 note         = "Graduate Texts in Computer Science",
)
@inbook(Buchb_Loos:82,
 author       = "Bruno Buchberger and R. Loos",
 year         = "1982",
 title        = "{Computer Algebra - Symbolic and Algebraic Computation}",
 chapter      = "Algebraic Simplification",
 pages        = "11--44",
 publisher    = "Springer, Vienna, New York",
)
@book(bk:dij90,
 author       = "Edsger W. Dijkstra and Carel S. Scholten",
 year         = "1990",
 title        = "Predicate Calculus and Program Semantics",
 series       = "Texts and Monographs in Computer Science",
 publisher    = "Springer verlag",
 address      = "New York",
)
@inproceedings(DBLP:conf/ascm/Gonthier07,
 author       = "Georges Gonthier",
 year         = "2007",
 title        = "The Four Colour Theorem: Engineering of a Formal Proof",
 editor       = "Deepak Kapur",
 booktitle    = "ASCM",
 series       = "Lecture Notes in Computer Science",
 volume       = "5081",
 publisher    = "Springer",
 pages        = "333",
 doi          = "10.1007/978-3-540-87827-8\_28",
)
@article(gries:calc-proof,
 author       = "D. Gries and F. Schneider",
 year         = "1995",
 title        = "Teaching math more effectively through calculational proofs",
 journal      = "Am. Math. Monthly",
 pages        = "691--697",
 doi          = "10.2307/2974638",
)
@article(plmms10,
 author       = "Florian Haftmann and Cezary Kaliszyk and Walther Neuper",
 year         = "2010",
 title        = "{CTP}-based programming languages~? Considerations about an experimental design",
 journal      = "ACM Communications in Computer Algebra",
 volume       = "44",
 number       = "1/2",
 pages        = "27--41",
 doi          = "10.1145/1838599.1838621",
)
@book(harr:book,
 author       = "John R. Harrison",
 year         = "1998",
 title        = "Theorem proving with the real numbers",
 series       = "Distinguished Dissertations",
 publisher    = "Springer",
 doi          = "10.1007/978-1-4471-1591-5",
)
@manual(Huet_all:94,
 author       = "G. Huet and G. Kahn and C. Paulin-Mohring",
 year         = "1994",
 title        = "The Coq Proof Assistant",
 address      = "CNRS-ENS Lyon",
)
@article(seeingroots,
 author       = "D.J. Jeffrey and A.C. Norman",
 year         = "2004",
 title        = "Not seeing the roots for the branches: multivalued functions in computer algebra",
 journal      = "SIGSAM Bull.",
 volume       = "38",
 number       = "3",
 pages        = "57--66",
 doi          = "10.1145/1040034.1040036",
)
@phdthesis(cezary-phd,
 author       = "Cezary Kalisyk",
 year         = "2009",
 title        = "Correctness and Availability. Building Computer Algebra on top of Proof Assistants and making Proof Assistants available over the Web",
 type         = "Ipa dissertation series 2009-18",
 school       = "Radboud University Nijmegen",
 note         = "Promotor Herman Geuvers",
)
@inproceedings(caspartial,
 author       = "Cezary Kaliszyk",
 year         = "2008",
 title        = "Automating Side Conditions in Formalized Partial Functions",
 editor       = "Serge Autexier and John Campbell and Julio Rubio and Volker Sorge and Masakazu Suzuki and Freek Wiedijk",
 booktitle    = "AISC/MKM/Calculemus",
 series       = "LNCS",
 volume       = "5144",
 publisher    = "Springer",
 pages        = "300--314",
 doi          = "10.1007/978-3-540-85110-3\_26",
)
@inproceedings(casproto,
 author       = "Cezary Kaliszyk and Freek Wiedijk",
 year         = "2007",
 title        = "Certified Computer Algebra on Top of an Interactive Theorem Prover",
 editor       = "Manuel Kauers and Manfred Kerber and Robert Miner and Wolfgang Windsteiger",
 booktitle    = "Calculemus",
 series       = "LNCS",
 volume       = "4573",
 publisher    = "Springer",
 pages        = "94--105",
 doi          = "10.1007/978-3-540-73086-6\_8",
)
@inproceedings(kremp.np:assess,
 author       = "Alan Krempler and Walther Neuper",
 year         = "2008",
 title        = "Formative Assessment for User Guidance in Single Stepping Systems",
 editor       = "Michael E. Aucher",
 booktitle    = "Interactive Computer Aided Learning, Proceedings of ICL08",
 address      = "Villach, Austria",
)
@incollection(pl:formal-lang-hist,
 author       = "Peter Lucas",
 year         = "1978",
 title        = "On the Formalization of Programming Languages: Early History and Main Approaches",
 editor       = "D. Bj{\o }rner and C. B. Jones",
 booktitle    = "The Vienna Development Method: The Meta-Language",
 series       = "LNCS",
 volume       = "16",
 publisher    = "Springer",
 doi          = "10.1007/3-540-08766-4\_8",
)
@article(pl:form-sem-VDL,
 author       = "Peter Lucas",
 year         = "1981",
 title        = "Formal Semantics of Programming Languages: {VDL}",
 journal      = "IBM Journal of Devt. and Res.",
 volume       = "25",
 number       = "5",
)
@book(pl:lucas70a,
 author       = "Peter Lucas and Kurt Walk",
 year         = "1970",
 title        = "On the Formal Description of PL/I",
 series       = "Annual Review in Automatic Programming",
 volume       = "6",
 publisher    = "Pergamon Press",
 address      = "Oxford",
)
@inproceedings(luth.ea:tas:2000,
 author       = "Christoph L{\"u}th and Burkhart Wolff",
 year         = "2000",
 title        = "{TAS} --- A Generic Window Inference System",
 editor       = "J. Harrison and M. Aagaard",
 booktitle    = "Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000",
 series       = "Lecture Notes in Computer Science",
 volume       = "1869",
 publisher    = "Springer Verlag",
 pages        = "405--422",
 doi          = "10.1007/3-540-44659-1\_25",
)
@book(progr-mathematica,
 author       = "Roman E. Maeder",
 year         = "1997",
 title        = "Programming in Mathematica",
 publisher    = "Addison-Wesley",
 address      = "Reading, Mass.",
)
@incollection(mw:isar07,
 author       = "Wenzel Makarius",
 year         = "2007",
 title        = "Isabelle/{I}sar --- a generic framework for human-readable proof documents",
 editor       = "R. Matuszewski and A. Zalewska",
 booktitle    = "From Insight to Proof --- Festschrift in Honour of Andrzej Trybulec",
 series       = "Studies in Logic, Grammar, and Rhetoric",
 volume       = "10",
 address      = "University of Bialystok",
)
@techreport(imst-htl06-SH,
 author       = "Walther Neuper",
 year         = "2006",
 title        = "{Angewandte Mathematik und Fachtheorie}",
 type         = "Technical Report",
 number       = "357",
 institution  = "Institute of Instructional and School Development (IUS)",
 address      = "University of Klagenfurt, Austria",
)
@techreport(imst-htl07-SH,
 author       = "Walther Neuper",
 year         = "2007",
 title        = "{Angewandte Mathematik und Fachtheorie}",
 type         = "Technical Report",
 number       = "683",
 institution  = "Institute of Instructional and School Development (IUS)",
 address      = "University of Klagenfurt, Austria",
)
@article(wn-cadgme09,
 author       = "Walther Neuper",
 year         = "2010",
 title        = "Common grounds for modelling mathematics in educational software",
 journal      = "Int. Journal for Technology in Mathematics Education",
 volume       = "17",
 number       = "3",
)
@techreport(imst-hpts08-SH,
 author       = "Walther Neuper and Johannes Reitinger",
 year         = "2008",
 title        = "{Begreifen und Mechanisieren beim Algebra Einstieg}",
 type         = "Technical Report",
 number       = "1063",
 institution  = "Institute of Instructional and School Development (IUS)",
 address      = "University of Klagenfurt, Austria",
)
@book(Nipkow-Paulson-Wenzel:2002,
 author       = "Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel",
 year         = "2002",
 title        = "{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic",
 series       = "LNCS",
 volume       = "2283",
 publisher    = "Springer",
 doi          = "10.1007/3-540-08766-4\_8",
)
@phdthesis(russellphd,
 author       = "Russell O'Connor",
 year         = "2009",
 title        = "Incompleteness and Completeness.",
 school       = "Radboud University Nijmegen",
)
@techreport(op-sem,
 author       = "Gordon D. Plotkin",
 year         = "1981",
 title        = "A structural approach to operational semantics",
 type         = "Technical Report",
 number       = "DAIMI FN-19",
 institution  = "CS, Aarhus University",
)
@techreport(rocard07-short,
 author       = "Michel Rocard and al.",
 year         = "2007",
 title        = "Science Education {NOW}: A Renewed Pedagogy for the Future of Europe",
 type         = "Technical Report",
 institution  = "European Communities, Directorate-General for Research",
)
@manual(isar-impl,
 author       = "Makarius Wenzel",
 year         = "2011",
 title        = "The {Isabelle/Isar} Implementation",
 address      = "(included in the {Isabelle} distribution)",
 note         = "With contributions by Florian Haftmann and Larry Paulson",
)
@inproceedings(makar:calc01,
 author       = "Markus Wenzel and Gertrud Bauer",
 year         = "2001",
 title        = "Calculational reasoning revisited - an {Isabelle/Isar} experience",
 editor       = "R. J. Boulton and P. B. Jackson",
 booktitle    = "Theorem Proving in Higher Order Logics",
 series       = "LNCS",
 volume       = "2152",
 organization = "TPHOLs 2001",
 publisher    = "Springer",
 doi          = "10.1007/3-540-44755-5\_7",
)