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