×

zbMATH — the first resource for mathematics

Imperative functional programming with Isabelle/HOL. (English) Zbl 1165.68352
Mohamed, Otmane Ait (ed.) et al., Theorem proving in higher order logics. 21st international conference, TPHOLs 2008, Montreal, Canada, August 18–21, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-71065-3/pbk). Lecture Notes in Computer Science 5170, 134-149 (2008).
Summary: We introduce a lightweight approach for reasoning about programs involving imperative data structures using the proof assistant Isabelle/HOL. It is based on shallow embedding of programs, a polymorphic heap model using enumeration encodings and type classes, and a state-exception monad similar to known counterparts from Haskell. Existing proof automation tools are easily adapted to provide a verification environment. The framework immediately allows for correct code generation to ML and Haskell. Two case studies demonstrate our approach: An array-based checker for resolution proofs, and a more efficient bytecode verifier.
For the entire collection see [Zbl 1149.68013].

MSC:
68N18 Functional programming and lambda calculus
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Boyer, R.S., Moore, J.S.: Single-threaded objects in ACL2. In: Krishnamurthi, S., Ramakrishnan, C.R. (eds.) PADL 2002. LNCS, vol. 2257, pp. 9–27. Springer, Heidelberg (2002) · doi:10.1007/3-540-45587-6_3
[2] Een, N., Sörensson, N.: An extensible sat-solver. In: Goos, G., Hartmanis, J., van Leeuwen, J. (eds.) SAT 2003. LNCS, vol. 2919, p. 502. Springer, Heidelberg (2004) · Zbl 1204.68191 · doi:10.1007/978-3-540-24605-3_37
[3] Filliâtre, J.-C., Marché, C.: The Why/Krakatoa/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590. Springer, Heidelberg (2007) · Zbl 05216226 · doi:10.1007/978-3-540-73368-3_21
[4] Haftmann, F., Nipkow, T.: A code generator framework for Isabelle/HOL. Technical Report 364/07, Department of Computer Science, University of Kaiserslautern (August 2007)
[5] Huffman, B., Matthews, J., White, P.: Axiomatic constructor classes in Isabelle/HOLCF. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 147–162. Springer, Heidelberg (2005) · Zbl 1152.68521 · doi:10.1007/11541868_10
[6] Jones, S.P., Launchbury, J.: Lazy functional state threads. In: SIGPLAN Conference on Programming Language Design and Implementation, pp. 24–35 (1994)
[7] Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. ACM Trans. Program. Lang. Syst. 28(4), 619–695 (2006) · doi:10.1145/1146809.1146811
[8] Krstić, S., Matthews, J.: Verifying BDD algorithms through monadic interpretation. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol. 2294, pp. 182–195. Springer, Heidelberg (2002) · Zbl 1057.68629 · doi:10.1007/3-540-47813-2_13
[9] Müller, O., Nipkow, T., Oheimb, D.V., Slotosch, O.: HOLCF = HOL + LCF. Journal of Functional Programming 9, 191–223 (1999) · Zbl 0933.03028 · doi:10.1017/S095679689900341X
[10] Nanevski, A., Morrisett, G., Birkedal, L.: Polymorphism and separation in hoare type theory. In: ICFP 2006: Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, pp. 62–73. ACM Press, New York (2006) · Zbl 1321.68351 · doi:10.1145/1159803.1159812
[11] Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002) · doi:10.1007/3-540-45949-9
[12] Obua, S.: Partizan games in Isabelle/HOLZF. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol. 4281, pp. 272–286. Springer, Heidelberg (2006) · Zbl 1168.68543 · doi:10.1007/11921240_19
[13] Jones, S.P., Wadler, P.: Imperative functional programming. In: Proc. 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1993), pp. 71–84 (1993) · doi:10.1145/158511.158524
[14] Schirmer, N.: A verification environment for sequential imperative programs in Isabelle/HOL. In: Baader, F., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, vol. 3452, pp. 398–414. Springer, Heidelberg (2005) · Zbl 1108.68410 · doi:10.1007/978-3-540-32275-7_26
[15] Sprenger, C., Basin, D.A.: A monad-based modeling and verification toolbox with application to security protocols. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 302–318. Springer, Heidelberg (2007) · Zbl 1144.68306 · doi:10.1007/978-3-540-74591-4_23
[16] Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: Hofmann, M., Felleisen, M. (eds.) Proc. 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2007), Nice, France, January 2007, pp. 97–108 (2007) · Zbl 1295.68094 · doi:10.1145/1190216.1190234
[17] Weber, T., Amjad, H.: Efficiently checking propositional refutations in HOL theorem provers. Journal of Applied Logic (to appear, 2007) · Zbl 1171.68041
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.