J.R. Abrial (1996):
The B Book: Assigning Programs to Meanings.
Cambridge University Press,
doi:10.1017/CBO9780511624162.
R. Bonichon, D. Delahaye & D. Doligez (2007):
Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs.
In: Logic for Programming, Artificial Intelligence, and Reasoning, 14th Int. Conf., LPAR,
LNCS 4790.
Springer,
pp. 151–165,
doi:10.1007/978-3-540-75560-9_13.
S. Boulmé, T. Hardin & R. Rioboo (2001):
Some hints for polynomials in the Foc project.
In: 9th Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2001.
A. Bove, P. Dybjer & U. Norell (2009):
A Brief Overview of Agda - A Functional Language with Dependent Types.
In: Theorem Proving in Higher Order Logics, 22nd Int. Conf., TPHOLs 2009, Proceedings,
LNCS 5674.
Springer,
pp. 73–78,
doi:10.1007/978-3-642-03359-9_6.
M. Carlier, C. Dubois & A. Gotlieb (2010):
Constraint Reasoning in FocalTest.
In: ICSOFT 2010 - Proceedings of the Fifth Int. Conf. on Software and Data Technologies, Volume 2.
SciTePress,
pp. 82–91.
K. Chaudhuri, D. Doligez, L. Lamport & S. Merz (2008):
A TLA^+ Proof System.
In: Proc. of the LPAR Workshops: Knowledge Exchange: Automated Provers and Proof Assistants, and The 7th Int. Workshop on the Implementation of Logics (KEAPPA).
Common Criteria (2005):
Common Criteria for Information Technology Security Evaluation, Norme ISO 15408 – Version 3.0 Rev 2.
D. Delahaye, M. Jaume & V. Prevosto (2005):
Coq: un outil pour l'enseignement.
Technique et Science Informatiques (TSI) 24(9),
pp. 1139–1160,
doi:10.3166/tsi.24.1139-1160.
K. Doets & J. van Eijck (2004):
The Haskell Road to Logic, Maths and Programming.
King's College Publications, London.
Focalize (2010):
Focalize, Tutorial and reference manual.
Distribution available at: http://focalize.inria.fr.
J. Harrison (2009):
Handbook of Practical Logic and Automated Reasoning.
Cambridge University Press,
doi:10.1007/s10817-012-9251-8.
P. B. Henderson (2002):
Functional and declarative languages for learning discrete mathematics.
In: Proceedings of the Int. Workshop on Functional & Declarative Programming in Education (FDPE 2002): Published as Technical Report No. 0210 of the University of Kiel (Germany).
M. Hendriks, C. Kaliszyk, F. van Raamsdonk & F. Wiedijk (2010):
Teaching logic using a state-of-the-art proof assistant.
Acta Didactica Napocensia 3(2),
pp. 35–48.
L. Lamport (1995):
How to Write a Proof.
AMM: The American Mathematical Monthly 102(7),
pp. 600–608,
doi:10.2307/2974556.
T. Nipkow (2012):
Teaching Semantics with a Proof Assistant: No more LSD Trip Proofs.
In: Verification, Model Checking, and Abstract Interpretation (VMCAI 2012),
LNCS 7148.
Springer,
pp. 24–38,
doi:10.1007/978-3-642-27940-9_3.
J. T. O'Donnell, C. V. Hall & R. Page (2006):
Discrete mathematics using a computer.
Springer,
doi:10.1007/1-84628-598-4.
R.L. Page (2003):
Software is discrete mathematics.
In: Proc. of the Eighth ACM SIGPLAN Int. Conf. on Functional Programming, ICFP 2003.
ACM,
pp. 79–86,
doi:10.1145/944746.944713.
B. C. Pierce (2009):
Lambda, the ultimate TA: using a proof assistant to teach programming language foundations.
In: Proc. of the 14th ACM SIGPLAN Int. Conf. on Functional programming, ICFP 2009.
ACM,
pp. 121–122,
doi:10.1007/978-3-642-27940-9_3.
V. Prevosto & D. Doligez (2002):
Algorithms and Proof Inheritance in the Foc language.
Journal of Automated Reasoning 29(3-4),
pp. 337–363,
doi:10.1023/A:1021979218446.
V. Prevosto & M. Jaume (2003):
Making proofs in a hierarchy of mathematical structures.
In: 11th Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2003.
Aracne,
pp. 89–100.
R. Rioboo (2009):
Invariants for the FoCaL language.
Annals of Mathematics and Artificial Intelligence 56(3-4),
pp. 273–296,
doi:10.1007/s10472-009-9156-3.
S. Da Rosa (2002):
The Role of Discrete Mathematics and Programming in Education.
In: Proceedings of the Int. Workshop on Functional & Declarative Programming in Education (FDPE 2002): Published as Technical Report No. 0210 of the University of Kiel (Germany).
C. Scharff & A. Wildenberg (2002):
Teaching Discrete Structures with SML.
In: Proceedings of the Int. Workshop on Functional & Declarative Programming in Education (FDPE 2002): Published as Technical Report No. 0210 of the University of Kiel (Germany).
T. VanDrunen (2011):
The case for teaching functional programming in discrete math.
In: C. Videira Lopes & K. Fisher: Companion to the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2011, part of SPLASH 2011.
ACM,
pp. 81–86,
doi:10.1145/2048147.2048180.
T. VanDrunen (2012):
Discrete mathematics and Functional Programming.
Franklin, Beedle and Associates.
R. L. Wainwright (1992):
Introducing functional programming in discrete mathematics.
In: N. B. Dale: Proc. of the 23rd SIGCSE Technical Symp. on Computer Science Education.
ACM,
pp. 147–152,
doi:10.1145/134510.134540.