@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",
)