References

  1. J.R. Abrial (1996): The B Book: Assigning Programs to Meanings. Cambridge University Press, doi:10.1017/CBO9780511624162.
  2. 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.
  3. 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.
  4. 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.
  5. 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.
  6. 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).
  7. Common Criteria (2005): Common Criteria for Information Technology Security Evaluation, Norme ISO 15408 – Version 3.0 Rev 2.
  8. 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.
  9. K. Doets & J. van Eijck (2004): The Haskell Road to Logic, Maths and Programming. King's College Publications, London.
  10. Focalize (2010): Focalize, Tutorial and reference manual. Distribution available at: http://focalize.inria.fr.
  11. J. Harrison (2009): Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, doi:10.1007/s10817-012-9251-8.
  12. 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).
  13. 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.
  14. L. Lamport (1995): How to Write a Proof. AMM: The American Mathematical Monthly 102(7), pp. 600–608, doi:10.2307/2974556.
  15. 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.
  16. T. Nipkow & G. Klein (2013): Concrete Semantics. A proof assistant approach. Draft. Available at http://www21.in.tum.de/~nipkow/Concrete-Semantics/concrete_semantics.pdf.
  17. J. T. O'Donnell, C. V. Hall & R. Page (2006): Discrete mathematics using a computer. Springer, doi:10.1007/1-84628-598-4.
  18. 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.
  19. 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.
  20. 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.
  21. 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.
  22. 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.
  23. 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).
  24. 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).
  25. 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.
  26. T. VanDrunen (2012): Discrete mathematics and Functional Programming. Franklin, Beedle and Associates.
  27. 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.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org