A Hoare Logic for Call-by-Value Functional Programs

1. Floyd, R.W.: Assigning meanings to programs. In: Mathematical Aspects of Computer Science. Proceedings of Symposia in Applied Mathematics, vol. 19, pp. 19–32. American Mathematical Society (1967)

   Google Scholar 

2. Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10), 576–580 (1969)

   Article  MATH  Google Scholar 

3. Cousot, P.: Methods and logics for proving programs. In: Formal Models and Semantics. Handbook of Theoretical Computer Science, vol. B, pp. 841–993. Elsevier Science, Amsterdam (1990)

   Google Scholar 

4. Clarke, E.: Programming language constructs for which it is impossible to obtain good Hoare axiom systems. Journal of the ACM 26(1), 129–147 (1979)

   Article  MATH  Google Scholar 

5. Apt, K.R.: Ten years of Hoare’s logic: A survey—part I. ACM Transactions on Programming Languages and Systems 3(4), 431–483 (1981)

   Article  MATH  Google Scholar 

6. Damm, W., Josko, B.: A sound and relatively^* complete axiomatization of Clarke’s language L4. In: Clarke, E., Kozen, D. (eds.) Logic of Programs 1983. LNCS, vol. 164, pp. 161–175. Springer, Heidelberg (1984)

   Google Scholar 

7. German, S., Clarke, E., Halpern, J.: Reasoning about procedures as parameters. In: Clarke, E., Kozen, D. (eds.) Logic of Programs 1983. LNCS, vol. 164, pp. 206–220. Springer, Heidelberg (1984)

   Google Scholar 

8. Goerdt, A.: A Hoare calculus for functions defined by recursion on higher types. In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol. 193, pp. 106–117. Springer, Heidelberg (1985)

   Google Scholar 

9. Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer 7(3), 212–232 (2005)

   Article  Google Scholar 

10. Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: ACM Conference on Programming Language Design and Implementation (PLDI), pp. 234–245 (2002)

    Google Scholar 

11. Marché, C., Paulin-Mohring, C., Urbain, X.: The Krakatoa tool for certification of Java/JavaCard programs annotated in JML. Journal of Logic and Algebraic Programming 58(1–2), 89–106 (2004)

    Article  MATH  Google Scholar 

12. Filliâtre, J.C., Marché, C.: Multi-prover Verification of C Programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 15–29. Springer, Heidelberg (2004)

    Google Scholar 

13. Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# Programming System: An Overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)

    Google Scholar 

14. Hughes, J.: Why functional programming matters. Computer Journal 32(2), 98–107 (1989)

    Article  Google Scholar 

15. Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic. Information and Computation 199(1–2), 200–227 (2005)

    Article  MathSciNet  MATH  Google Scholar 

16. Detlefs, D.L., Leino, K.R.M., Nelson, G.: Wrestling with rep exposure. Research Report 156, SRC (July 1998)

    Google Scholar 

17. Leino, K.R.M., Nelson, G.: Data abstraction and information hiding. ACM Transactions on Programming Languages and Systems 24(5), 491–553 (2002)

    Article  Google Scholar 

18. Fähndrich, M., DeLine, R.: Adoption and focus: practical linear types for imperative programming. In: ACM Conference on Programming Language Design and Implementation (PLDI), pp. 13–24 (June 2002)

    Google Scholar 

19. Clarke, D.G., Potter, J.M., Noble, J.: Ownership types for flexible alias protection. In: ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pp. 48–64 (October 1998)

    Google Scholar 

20. Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: IEEE Symposium on Logic in Computer Science (LICS), pp. 55–74 (2002)

    Google Scholar 

21. Régis-Gianas, Y.: A Hoare logic for call-by-value functional programs: Prototype tool (January 2008), http://pangolin-programming-language.googlecode.com

22. The Coq development team: The Coq Proof Assistant (2006)

    Google Scholar 

23. Conchon, S., Contejean, E.: The Alt-Ergo automatic theorem prover (2006), http://alt-ergo.lri.fr/

24. Kaplan, H., Tarjan, R.E.: Purely functional, real-time deques with catenation. Journal of the ACM 46(5), 577–603 (1999)

    Article  MathSciNet  MATH  Google Scholar 

25. Milner, R.: A theory of type polymorphism in programming. Journal of Computer and System Sciences 17(3), 348–375 (1978)

    Article  MathSciNet  MATH  Google Scholar 

26. Xi, H.: Dependent Types in Practical Programming. PhD thesis, Carnegie Mellon University (December 1998)

    Google Scholar 

27. Leroy, X., Doligez, D., Garrigue, J., Rémy, D., Vouillon, J.: The Objective Caml system (October 2005)

    Google Scholar 

28. Andrews, P.B.: An introduction to mathematical logic and type theory: to truth through proof. Academic Press, London (1986)

    MATH  Google Scholar 

29. Paulin-Mohring, C.: Inductive definitions in the system Coq: rules and properties. Research Report RR1992-49, ENS Lyon (1992)

    Google Scholar 

30. Werner, B.: Une Théorie des Constructions Inductives. PhD thesis, Université Paris 7 (1994)

    Google Scholar 

31. Flanagan, C., Sabry, A., Duba, B.F., Felleisen, M.: The essence of compiling with continuations. In: ACM Conference on Programming Language Design and Implementation (PLDI), pp. 237–247 (1993)

    Google Scholar 

32. Régis-Gianas, Y.: Des types aux assertions logiques: preuve automatique ou assistée de propriétés sur les programmes fonctionnels. PhD thesis, Université Paris 7 (November 2007)

    Google Scholar 

33. Nanevski, A., Ahmed, A., Morrisett, G., Birkedal, L.: Abstract Predicates and Mutable ADTs in Hoare Type Theory. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 189–204. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

34. Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. Journal of the ACM 52(3), 365–473 (2005)

    Article  MathSciNet  Google Scholar 

35. Lescuyer, S.: Codage de la logique du premier ordre polymorphe multi-sortée dans la logique sans sortes. Master’s thesis, Master Parisien de Recherche en Informatique (2006)

    Google Scholar 

36. Kerber, M.: How to prove higher order theorems in first order logic. In: International Joint Conferences on Artificial Intelligence, pp. 137–142 (1991)

    Google Scholar 

37. Altenkirch, T., McBride, C., McKinna, J.: Why dependent types matter (unpublished) (April 2005)

    Google Scholar 

38. Sozeau, M.: Subset coercions in Coq. In: TYPES (2006)

    Google Scholar 

39. Xi, H., Chen, C., Chen, G.: Guarded recursive datatype constructors. In: ACM Symposium on Principles of Programming Languages (POPL), pp. 224–235 (January 2003)

    Google Scholar 

40. Filliâtre, J.C.: Backtracking iterators. In: ACM Workshop on ML (September 2006)

    Google Scholar 

41. Detlefs, D.L., Leino, K.R.M., Nelson, G., Saxe, J.B.: Extended static checking. Research Report 159, Compaq SRC (December 1998)

    Google Scholar 

42. Filliâtre, J.C.: Why: a multi-language multi-prover verification tool. Research Report 1366, LRI, Université Paris Sud (March 2003)

    Google Scholar 

43. Flanagan, C., Saxe, J.B.: Avoiding exponential explosion: generating compact verification conditions. In: ACM Symposium on Principles of Programming Languages (POPL), pp. 193–205 (2001)

    Google Scholar 

44. Scott, D.S.: A type-theoretical alternative to ISWIM, CUCH, OWHY. Theoretical Computer Science 121(1–2), 411–440 (1993)

    Article  MathSciNet  MATH  Google Scholar 

45. Milner, R.: Implementation and applications of Scott’s logic for computable functions. In: Proceedings of the ACM conference on proving assertions about programs, pp. 1–6 (January 1972)

    Google Scholar 

46. Agerholm, S.: A HOL basis for reasoning about functional programs. Technical Report RS-94-44, BRICS (December 1994)

    Google Scholar 

47. Bartels, F., von Henke, F., Pfeifer, H., Rueß, H.: Mechanizing domain theory. Ulmer Informatik-Berichte 96-10, Universität Ulm, Fakultät für Informatik (1996)

    Google Scholar 

48. Müller, O., Nipkow, T., von Oheimb, D., Slotosch, O.: HOLCF = HOL + LCF. Journal of Functional Programming 9, 191–223 (1999)

    Article  MathSciNet  MATH  Google Scholar 

49. Longley, J., Pollack, R.: Reasoning About CBV Functional Programs in Isabelle/HOL. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 201–216. Springer, Heidelberg (2004)

    Google Scholar 

50. Kieburtz, R.B.: P -logic: Property verification for Haskell programs. Draft (August 2002)

    Google Scholar 

51. Hallgren, T., Hook, J., Jones, M.P., Kieburtz, R.: An overview of the Programatica toolset. In: High Confidence Software and Systems Conference (HCSS) (2004)

    Google Scholar 

52. Abel, A., Benke, M., Bove, A., Hughes, J., Norell, U.: Verifying Haskell programs using constructive type theory. In: Haskell workshop, pp. 62–73 (September 2005)

    Google Scholar 

53. Honda, K., Yoshida, N.: A compositional logic for polymorphic higher-order functions. In: International ACM Conference on Principles and Practice of Declarative Programming (PPDP), pp. 191–202 (August 2004)

    Google Scholar 

54. Smith, S.F.: Partial Objects in Type Theory. PhD thesis, Cornell University (January 1989)

    Google Scholar 

55. Xu, D.N.: Extended static checking for Haskell. In: Haskell workshop, pp. 48–59. ACM Press, New York (2006)

    Chapter  Google Scholar 

56. Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: ACM Symposium on Principles of Programming Languages (POPL), pp. 42–54 (January 2006)

    Google Scholar 

57. Nanevski, A., Morrisett, G., Birkedal, L.: Polymorphism and separation in Hoare type theory. In: ACM International Conference on Functional Programming (ICFP), pp. 62–73 (September 2006)

    Google Scholar 

58. Barnett, M., Naumann, D.A., Schulte, W., Sun, Q.: 99.44% pure: Useful abstractions in specifications. In: Formal Techniques for Java-like Programs (2004)

    Google Scholar 

59. Gronski, J., Knowles, K., Tomb, A., Freund, S.N., Flanagan, C.: Sage: Hybrid checking for flexible specifications. In: Scheme and Functional Programming (September 2006)

    Google Scholar 

60. Zenger, C.: Indexed types. Theoretical Computer Science 187(1–2), 147–165 (1997)

    Article  MathSciNet  MATH  Google Scholar 

61. Davies, R.: Practical refinement-type checking. Technical Report CMU-CS-05-110, School of Computer Science, Carnegie Mellon University (May 2005)

    Google Scholar 

62. Pottier, F., Régis-Gianas, Y.: Towards efficient, typed LR parsers. In: ACM Workshop on ML. Electronic Notes in Theoretical Computer Science, vol. 148(2), pp. 155–180 (March 2006)

    Google Scholar 

63. Pottier, F., Régis-Gianas, Y.: Stratified type inference for generalized algebraic data types. In: ACM Symposium on Principles of Programming Languages (POPL) (January 2006)

    Google Scholar 

64. Chen, C., Xi, H.: Combining programming with theorem proving. In: ACM International Conference on Functional Programming (ICFP) (September 2005)

    Google Scholar 

65. Sheard, T.: Putting Curry-Howard to work. In: Haskell workshop (2005)

    Google Scholar 

66. Westbrook, E., Stump, A., Wehrman, I.: A language-based approach to functionally correct imperative programming. In: ACM International Conference on Functional Programming (ICFP), pp. 268–279 (2005)

    Google Scholar 

Download references