Abstract
We describe a course on the semantics of a simple imperative programming language and on applications to compilers, type systems, static analyses and Hoare logic. The course is entirely based on the proof assistant Isabelle and includes a compact introduction to Isabelle. The overall aim is to teach the students how to write correct and readable proofs.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Aaronson, S.: Teaching statement (2007), http://www.scottaaronson.com/teaching.pdf
Berghofer, S., Bulwahn, L., Haftmann, F.: Turning Inductive into Equational Specifications. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 131–146. Springer, Heidelberg (2009)
Berghofer, S., Nipkow, T.: Executing Higher Order Logic. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol. 2277, pp. 24–40. Springer, Heidelberg (2002)
Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic Proof and Disproof in Isabelle/HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCos 2011. LNCS, vol. 6989, pp. 12–27. Springer, Heidelberg (2011)
Cachera, D., Pichardie, D.: A Certified Denotational Abstract Interpreter. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 9–24. Springer, Heidelberg (2010)
Klein, G.: Interactive proof: Applications to semantics. In: Proc. Summer School Marktoberdorf 2011 (to appear, 2012)
Leroy, X.: Coinductive Big-Step Operational Semantics. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 54–68. Springer, Heidelberg (2006)
Naumowicz, A., Korniłowicz, A.: A Brief Overview of Mizar. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 67–72. Springer, Heidelberg (2009)
Nielson, H.R., Nielson, F.: Semantics with Applications. Wiley (1992)
Nielson, H.R., Nielson, F.: Semantics with Applications. An Appatizer. Springer, Heidelberg (2007)
Nipkow, T.: Winskel is (Almost) Right: Towards a Mechanized Semantics Textbook. In: Chandru, V., Vinay, V. (eds.) FSTTCS 1996. LNCS, vol. 1180, pp. 180–192. Springer, Heidelberg (1996)
Nipkow, T.: Winskel is (almost) right: Towards a mechanized semantics textbook. Formal Aspects of Computing 10, 171–186 (1998)
Nipkow, T.: Interactive proof: Introduction to Isabelle/HOL. In: Proc. Summer School Marktoberdorf 2011 (to appear, 2012)
Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
Page, R.: Engineering software correctness. J. Functional Programming 17(6), 675–686 (2007)
Page, R., Eastlund, C., Felleisen, M.: Functional programming and theorem proving for undergraduates: A progress report. In: Proc. 2008 International Workshop on Functional and Declarative Programming in Education, FDPE 2008, pp. 21–30. ACM (2008)
Pierce, B.C.: Lambda, the ultimate TA: using a proof assistant to teach programming language foundations. In: Proc. 14th ACM SIGPLAN International Conference on Functional Programming, ICFP 2009, pp. 121–122. ACM (2009)
Urban, C.: Nominal techniques in Isabelle/HOL. J. Automated Reasoning 40, 327–356 (2008)
Vaillancourt, D., Page, R., Felleisen, M.: ACL2 in DrScheme. In: Manolios, P., Wilding, M. (eds.) Proc. Sixth International Workshop on the ACL2 Theorem Prover and its Applications, pp. 107–116. ACM (2006)
Volpano, D., Smith, G., Irvine, C.: A sound type system for secure flow analysis. Journal of Computer Security 4(2-3), 167–187 (1996)
Wenzel, M.: Isabelle/Isar — A Versatile Environment for Human-Readable Formal Proof Documents. PhD thesis, Institut für Informatik, Technische Universität München (2002)
Wenzel, M., Wiedijk, F.: A comparison of Mizar and Isar. J. Automated Reasoning, 389–411 (2002)
Winskel, G.: The Formal Semantics of Programming Languages. MIT Press (1993)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nipkow, T. (2012). Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs. In: Kuncak, V., Rybalchenko, A. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2012. Lecture Notes in Computer Science, vol 7148. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-27940-9_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-27940-9_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-27939-3
Online ISBN: 978-3-642-27940-9
eBook Packages: Computer ScienceComputer Science (R0)