@book(Abrial96a,
 author       = "J.R. Abrial",
 year         = "1996",
 title        = "The {B}~Book: Assigning Programs to Meanings",
 publisher    = "Cambridge University Press",
 doi          = "10.1017/CBO9780511624162",
)
@inproceedings(conf/lpar/BonichonDD07,
 author       = "R. Bonichon and D. Delahaye and D. Doligez",
 year         = "2007",
 title        = "Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs",
 booktitle    = "Logic for Programming, Artificial Intelligence, and Reasoning, 14th Int. Conf., {LPAR}",
 series       = "LNCS",
 volume       = "4790",
 publisher    = "Springer",
 pages        = "151--165",
 doi          = "10.1007/978-3-540-75560-9\_13",
)
@inproceedings(calc01,
 author       = "S. Boulm\'e and T. Hardin and R. Rioboo",
 year         = "2001",
 title        = "Some hints for polynomials in the {F}oc project",
 booktitle    = "9th Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2001",
)
@inproceedings(conf/tphol/BoveDN09,
 author       = "A. Bove and P. Dybjer and U. Norell",
 year         = "2009",
 title        = "A Brief Overview of {A}gda - {A} Functional Language with Dependent Types",
 booktitle    = "Theorem Proving in Higher Order Logics, 22nd Int. Conf., {TPHOL}s 2009, Proceedings",
 series       = "LNCS",
 volume       = "5674",
 publisher    = "Springer",
 pages        = "73--78",
 doi          = "10.1007/978-3-642-03359-9\_6",
)
@inproceedings(DBLP:conf/icsoft/CarlierDG10,
 author       = "M. Carlier and C. Dubois and A. Gotlieb",
 year         = "2010",
 title        = "Constraint Reasoning in {F}ocal{T}est",
 booktitle    = "ICSOFT 2010 - Proceedings of the Fifth Int. Conf. on Software and Data Technologies, Volume 2",
 publisher    = "SciTePress",
 pages        = "82--91",
)
@inproceedings(chaudhuri:proof,
 author       = "K. Chaudhuri and D. Doligez and L. Lamport and S. Merz",
 year         = "2008",
 title        = "A {TLA${}^{+}$} Proof System",
 booktitle    = "Proc. of the {LPAR} Workshops: Knowledge Exchange: Automated Provers and Proof Assistants, and The 7th Int. Workshop on the Implementation of Logics (KEAPPA)",
)
@manual(CC2,
 author       = "{Common Criteria}",
 year         = "2005",
 title        = "Common Criteria for Information Technology Security Evaluation, Norme {ISO} 15408 -- Version 3.0 Rev 2",
)
@article(Coq-Ens,
 author       = "D. Delahaye and M. Jaume and V. Prevosto",
 year         = "2005",
 title        = "{{Coq}: un outil pour l'enseignement}",
 journal      = "Technique et Science Informatiques (TSI)",
 volume       = "24",
 number       = "9",
 pages        = "1139--1160",
 doi          = "10.3166/tsi.24.1139-1160",
)
@book(Doets04,
 author       = "K. Doets and J. van Eijck",
 year         = "2004",
 title        = "The Haskell Road to Logic, Maths and Programming",
 publisher    = "King's College Publications, London",
)
@manual(foc03,
 author       = "Focalize",
 year         = "2010",
 title        = "{Focalize}, {Tutorial and reference manual}",
 note         = "Distribution available at: {\tt http://focalize.inria.fr}",
)
@book(Harrison09,
 author       = "J. Harrison",
 year         = "2009",
 title        = "Handbook of Practical Logic and Automated Reasoning",
 publisher    = "Cambridge University Press",
 doi          = "10.1007/s10817-012-9251-8",
)
@inproceedings(Henderson02,
 author       = "P. B. Henderson",
 year         = "2002",
 title        = "Functional and declarative languages for learning discrete mathematics",
 editor       = "Proceedings of the Int. Workshop on Functional and Declarative Programming in Education (FDPE 2002)",
 booktitle    = "Published as Technical Report No. 0210 of the University of Kiel (Germany)",
)
@article(hendriks-adn10,
 author       = "M. Hendriks and C. Kaliszyk and F. van Raamsdonk and F. Wiedijk",
 year         = "2010",
 title        = "Teaching logic using a state-of-the-art proof assistant",
 journal      = "Acta Didactica Napocensia",
 volume       = "3",
 number       = "2",
 pages        = "35--48",
)
@article(Lamport95,
 author       = "L. Lamport",
 year         = "1995",
 title        = "How to Write a Proof",
 journal      = "AMM: The American Mathematical Monthly",
 volume       = "102",
 number       = "7",
 pages        = "600--608",
 doi          = "10.2307/2974556",
)
@inproceedings(Nipkow-VMCAI12,
 author       = "T. Nipkow",
 year         = "2012",
 title        = "Teaching Semantics with a Proof Assistant: No more {LSD} Trip Proofs",
 booktitle    = "Verification, Model Checking, and Abstract Interpretation (VMCAI 2012)",
 series       = "LNCS",
 volume       = "7148",
 publisher    = "Springer",
 pages        = "24--38",
 doi          = "10.1007/978-3-642-27940-9\_3",
)
@book(NKtoappear,
 author       = "T. Nipkow and G. Klein",
 year         = "2013",
 title        = "Concrete Semantics. A proof assistant approach",
 publisher    = "Draft",
 url          = "http://www21.in.tum.de/~nipkow/Concrete-Semantics/concrete_semantics.pdf",
)
@book(books/daglib/0007497,
 author       = "J. T. O'Donnell and C. V. Hall and R. Page",
 year         = "2006",
 title        = "Discrete mathematics using a computer",
 publisher    = "Springer",
 doi          = "10.1007/1-84628-598-4",
)
@inproceedings(DBLP:conf/icfp/Page03,
 author       = "R.L. Page",
 year         = "2003",
 title        = "Software is discrete mathematics",
 booktitle    = "Proc. of the Eighth ACM SIGPLAN Int. Conf. on Functional Programming, ICFP 2003",
 publisher    = "ACM",
 pages        = "79--86",
 doi          = "10.1145/944746.944713",
)
@inproceedings(DBLP:conf/icfp/Pierce09,
 author       = "B. C. Pierce",
 year         = "2009",
 title        = "Lambda, the ultimate TA: using a proof assistant to teach programming language foundations",
 booktitle    = "Proc. of the 14th ACM SIGPLAN Int. Conf. on Functional programming, ICFP 2009",
 publisher    = "ACM",
 pages        = "121--122",
 doi          = "10.1007/978-3-642-27940-9\_3",
)
@article(PrevostoJAR02,
 author       = "V. Prevosto and D. Doligez",
 year         = "2002",
 title        = "Algorithms and Proof Inheritance in the {Foc} language",
 journal      = "Journal of Automated Reasoning",
 volume       = "29",
 number       = "3-4",
 pages        = "337--363",
 doi          = "10.1023/A:1021979218446",
)
@inproceedings(calc03,
 author       = "V. Prevosto and M. Jaume",
 year         = "2003",
 title        = "Making proofs in a hierarchy of mathematical structures",
 booktitle    = "11th Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2003",
 publisher    = "Aracne",
 pages        = "89--100",
)
@article(DBLP:journals/amai/Rioboo09,
 author       = "R. Rioboo",
 year         = "2009",
 title        = "Invariants for the {F}oCaL language",
 journal      = "Annals of Mathematics and Artificial Intelligence",
 volume       = "56",
 number       = "3-4",
 pages        = "273--296",
 doi          = "10.1007/s10472-009-9156-3",
)
@inproceedings(darosa02,
 author       = "S. Da Rosa",
 year         = "2002",
 title        = "The Role of Discrete Mathematics and Programming in Education",
 editor       = "Proceedings of the Int. Workshop on Functional and Declarative Programming in Education (FDPE 2002)",
 booktitle    = "Published as Technical Report No. 0210 of the University of Kiel (Germany)",
)
@inproceedings(oai:CiteSeerXPSU:10.1.1.19.3780,
 author       = "C. Scharff and A. Wildenberg",
 year         = "2002",
 title        = "Teaching Discrete Structures with {SML}",
 editor       = "Proceedings of the Int. Workshop on Functional and Declarative Programming in Education (FDPE 2002)",
 booktitle    = "Published as Technical Report No. 0210 of the University of Kiel (Germany)",
)
@inproceedings(DBLP:conf/oopsla/VanDrunen11,
 author       = "T. VanDrunen",
 year         = "2011",
 title        = "The case for teaching functional programming in discrete math",
 editor       = "C. Videira Lopes and K. Fisher",
 booktitle    = "Companion to the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2011, part of SPLASH 2011",
 publisher    = "ACM",
 pages        = "81--86",
 doi          = "10.1145/2048147.2048180",
)
@book(bookvandrunen,
 author       = "T. VanDrunen",
 year         = "2012",
 title        = "Discrete mathematics and Functional Programming",
 publisher    = "Franklin, Beedle and Associates",
)
@inproceedings(DBLP:conf/sigcse/Wainwright92,
 author       = "R. L. Wainwright",
 year         = "1992",
 title        = "Introducing functional programming in discrete mathematics",
 editor       = "N. B. Dale",
 booktitle    = "Proc. of the 23rd SIGCSE Technical Symp. on Computer Science Education",
 publisher    = "ACM",
 pages        = "147--152",
 doi          = "10.1145/134510.134540",
)