Abstract
During the past three years we have been integrating mechanized theorem proving into a traditional introductory course on formal methods. We explain our goals for adding mechanized provers to the course, and illustrate how we have integrated the provers into our syllabus to meet those goals. We also document some of the teaching materials we have developed for the course to date, and what our experiences have been like.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Andrews, P.B., Bishop, P., Brown, C.E., Issar, S., Pfenning, F., Xi, H.: ETPS: A system to help students write formal proofs (2003)
The ACL2 Sedan, http://acl2s.ccs.neu.edu/acl2s/doc
Asperti, A., Coen, C.S., Tassi, E., Zacchiroli, S.: User interaction with the matita proof assistant. Journal of Automated Reasoning 39(2), 109–139 (2007)
Aldrich, J., Simmons, R.J., Shin, K.: SASyLF: An educational proof assistant for language theory. In: 2008 ACM SIGPLAN Workshop on Functional and Declarative Programming Education (FDPE 2008), Victoria, BC, Canada (2008)
Ben-Ari, M.: Mathematical Logic for Computer Science. Springer, Heidelberg (2001)
Borchert, D.M. (ed.): Glossary of Logical Terms, 2nd edn. Encyclopedia of Philosophy. Macmillan (2006)
de Wind, P.: Modal logic in Coq. VU University Amsterdam, IR-488 (2001), http://www.cs.vu.nl/~tcs/mt/dewind.ps.gz
Henz, M., Hobor, A.: Course materials for cs3234/cs5209 (2010), http://www.comp.nus.edu.sg/~henz/cs3234
Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press (2000)
Huth, M.R.A., Ryan, M.D.: Logic in Computer Science: Modelling and reasoning about systems. Cambridge University Press, Cambridge (2000)
Nemhauser, G.L., Trick, M.A.: Scheduling a major college basketball conference. Operations Research 46(1), 1–8 (1998)
Ou, X., Govindavajhala, S., Appel, A.W.: MulVAL: A logic-based network security analyzer. In: 14th USENIX Security Symposium (2005)
Parry, W.T., Hacker, E.A.: Aristotelian Logic. State University of New York Press (1991)
Pierce, B.C.: Lambda, the ultimate TA: Using a proof assistant to teach programming language foundations (2009)
Zhang, H.: SATO: A decision procedure for propositional logic. Association of Automated Resasoning Newsletters 22 (1993, updated version of November 29) (1997)
Zhang, H.: Generating college conference basketball schedules by a SAT solver. In: Proceedings of the Fifth International Symposium on Theory and Applications of Satisfiability Testing, Cincinnati, Ohio, pp. 281–291 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Henz, M., Hobor, A. (2011). Teaching Experience: Logic and Formal Methods with Coq. In: Jouannaud, JP., Shao, Z. (eds) Certified Programs and Proofs. CPP 2011. Lecture Notes in Computer Science, vol 7086. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-25379-9_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-25379-9_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-25378-2
Online ISBN: 978-3-642-25379-9
eBook Packages: Computer ScienceComputer Science (R0)