Journal of Automated Reasoning

, Volume 50, Issue 4, pp 383–421 | Cite as

A Two-Valued Logic for Properties of Strict Functional Programs Allowing Partial Functions



A typed program logic LMF for recursive specification and verification is presented. It comprises a strict functional programming language with polymorphic and recursively defined partial functions and polymorphic data types. The logic is two-valued with the equality symbol as only predicate. Quantifiers range over the values, which permits inductive proofs of properties. The semantics is based on a contextual (observational) semantics, which gives a consistent presentation of higher-order functions. Our analysis also sheds new light on the the role of partial functions and loose specifications. It is also an analysis of influence of extensions of programs on the tautologies. The main result is that universally quantified equations are conservative, which is also the base for several other conservative classes of formulas.


Verification Functional programming Logics Semantics Contextual equivalence 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Supplementary material

10817_2012_9253_MOESM1_ESM.pdf (393 kb)
(PDF 392 KB)


  1. 1.
    ACL2 Website: (2011). Accessed 1 May 2012
  2. 2.
    Agda Website: (2011). Accessed 1 May 2012
  3. 3.
    Barendregt, H.P.: The Lambda Calculus. Its Syntax and Semantics. North-Holland, Amsterdam, New York (1984)Google Scholar
  4. 4.
    Barringer, H., Cheng, J.H., Jones, C.B.: A logic covering undefinedness in program proofs. Acta Inform. 21, 251–269 (1984)MathSciNetMATHCrossRefGoogle Scholar
  5. 5.
    Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer (2004)Google Scholar
  6. 6.
    Bertot, Y., Komendantsky, V.: Fixed point semantics and partial recursion in Coq. In: Antoy, S., Albert, E. (eds.) Proc. PPDP ’08, pp. 89–96. ACM, New York, NY, USA (2008)Google Scholar
  7. 7.
    Bove, A., Krauss, A., Sozeau, M.: Partiality and recursion in interactive theorem provers: an overview. Math. Struct. Comput. Sci. (2012, to appear). Preprint available at dates from 2011
  8. 8.
    Boyer, R.S., Moore, J.S.: Proving theorems about lisp functions. J. ACM 22(1), 129–144 (1975)MathSciNetMATHCrossRefGoogle Scholar
  9. 9.
    Boyer, R.S., Moore, J.S.: A mechanical proof of the unsolvability of the halting problem. J. ACM 31(3), 441–458 (1984)MathSciNetMATHCrossRefGoogle Scholar
  10. 10.
    Cheng, J.H., Jones, C.B.: On the usability of logics which handle partial functions. In: Morgan, C., Woodcock, J.C.P. (eds.) 3rd Refinement Workshop, pp. 51–69. Springer (1991)Google Scholar
  11. 11.
    Chiba, Y., Aoto, T., Toyama, Y.: Program transformation by templates based on term rewriting. In: Barahona, P., Felty, A.P. (eds.) Proc. PPDP ’05, pp. 59–69. ACM (2005)Google Scholar
  12. 12.
    Coq Website: (2011). Accessed 1 May 2012
  13. 13.
    Coquand, T., Huet, G.P.: The calculus of constructions. Inf. Comput. 76(2/3), 95–120 (1988)MathSciNetMATHCrossRefGoogle Scholar
  14. 14.
    Farmer, W.M.: A simple type theory with partial functions and subtypes. Ann. Pure Appl. Logic 64(3), 211–240 (1993)MathSciNetMATHCrossRefGoogle Scholar
  15. 15.
    Farmer, W.M.: Mechanizing the traditional approach to partial functions. In: Farmer, W., Kerber, M., Kohlhase, M. (eds.) Proceedings of the Workshop on the Mechanization of Partial Functions, pp. 27–32. CADE-13, Rutgers University, New Brunswick, New Jersey. Available from (1996). Accessed 1 May 2012
  16. 16.
    Farmer, W.M.: Formalizing undefinedness arising in calculus. In: Basin, D.A., Rusinowitch, M. (eds.) Proc. IJCAR ’04. Lecture Notes in Comput. Sci., vol. 3097, pp. 475–489. Springer (2004)Google Scholar
  17. 17.
    Farmer, W.M., Guttman, J.D., Thayer, F.J.: IMPS: an interactive mathematical proof system. J. Autom. Reason. 11(2), 213–248 (1993)MATHCrossRefGoogle Scholar
  18. 18.
    Felleisen, M., Hieb, R.: The revised report on the syntactic theories of sequential control and state. Theor. Comput. Sci. 103, 235–271 (1992)MathSciNetMATHCrossRefGoogle Scholar
  19. 19.
    Finn, S., Fourman, M.P., Longley, J.: Partial functions in a total setting. J. Autom. Reason. 18(1), 85–104 (1997)MathSciNetMATHCrossRefGoogle Scholar
  20. 20.
    Fitzgerald, J., Jones, C.: The connection between two ways of reasoning about partial functions. Inf. Process. Lett. 107(3–4), 128–132 (2008)MathSciNetMATHCrossRefGoogle Scholar
  21. 21.
    Giesl, J.: Induction proofs with partial functions. J. Autom. Reason. 26(1), 1–49 (2001)MathSciNetMATHCrossRefGoogle Scholar
  22. 22.
    Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, New York, NY, USA (1993)Google Scholar
  23. 23.
    Hähnle, R.: Many-valued logic, partiality, and abstraction in formal specification languages. Log. J. IGPL 13(4), 415–433 (2005)MathSciNetMATHCrossRefGoogle Scholar
  24. 24.
    HOL4 Website: (2011). Accessed 1 May 2012
  25. 25.
    Howe, D.: Equality in lazy computation systems. In: Parikh, R. (ed.) LICS ’89, pp. 198–203 (1989)Google Scholar
  26. 26.
    Howe, D.: Proving congruence of bisimulation in functional programming languages. Inf. Comput. 124(2), 103–112 (1996)MathSciNetMATHCrossRefGoogle Scholar
  27. 27.
    Isabelle/HOL Website: (2011). Accessed 1 May 2012
  28. 28.
    Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. Prentice Hall International Series in Computer Science. Prentice Hall (1991)Google Scholar
  29. 29.
    Kapur, D., Musser, D.R.: Inductive reasoning with incomplete specifications (preliminary report). In: Meyer, A. (ed.) LICS ’86, pp. 367–377. IEEE Computer Society (1986)Google Scholar
  30. 30.
    Klein, G., Nipkow, T., Paulson, L.: The archive of formal proofs. (2011). Accessed 1 May 2012
  31. 31.
    Krauss, A.: Partial recursive functions in higher-order logic. In: Furbach, U., Shankar, N. (eds.) Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, 17–20 August 2006, Proceedings. Lecture Notes in Comput. Sci., vol. 4130, pp. 589–603. Springer (2006)Google Scholar
  32. 32.
    Krauss, A.: Partial and nested recursive function definitions in higher-order logic. J. Autom. Reason. 44(4), 303–336 (2010)MathSciNetMATHCrossRefGoogle Scholar
  33. 33.
    Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)CrossRefGoogle Scholar
  34. 34.
    Mason, I., Talcott, C.L.: Equivalence in functional languages with effects. J. Funct. Program. 1(3), 287–327 (1991)MathSciNetMATHCrossRefGoogle Scholar
  35. 35.
    Morris, J.: Lambda-calculus models of programming languages. Ph.D. thesis, MIT (1968)Google Scholar
  36. 36.
    Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL — A Proof Assistant for Higher-Order Logic. Lecture Notes in Comput. Sci., vol. 2283. Springer (2002)Google Scholar
  37. 37.
    Pitts, A.M.: Operationally-based theories of program equivalence. In: Pitts, A.M., Dybjer, P. (eds.) Semantics and Logics of Computation. Cambridge University Press (1997)Google Scholar
  38. 38.
    Plotkin, G.D.: Call-by-name, call-by-value, and the lambda-calculus. Theor. Comput. Sci. 1, 125–159 (1975)MathSciNetMATHCrossRefGoogle Scholar
  39. 39.
    Sabel, D., Schmidt-Schauß, M., Harwath, F.: Reasoning about contextual equivalence: from untyped to polymorphically typed calculi. In: Fischer, S., Maehle, E., Reischuk, R. (eds.) INFORMATIK 2009. GI Edition - Lecture Notes in Informatics, vol. 154, pp. 369; 2931–2945 (2009)Google Scholar
  40. 40.
    Sands, D., Gustavsson, J., Moran, A.: Lambda calculi and linear speedups. In: Mogensen, T., Schmidt, D., Sudborough, I. (eds.) The Essence of Computation 2002, pp. 60–84. Springer (2002)Google Scholar
  41. 41.
    Schieder, B., Broy, M.: Adapting calculational logic to the undefined. Comput. J. 42(2), 73–81 (1999)MATHCrossRefGoogle Scholar
  42. 42.
    Schlosser, A., Walther, C., Gonder, M., Aderhold, M.: Context dependent procedures and computed types in verifun. Electron. Notes Theor. Comput. Sci. 174(7), 61–78 (2007)CrossRefGoogle Scholar
  43. 43.
    Schmidt-Schauß, M., Sabel, D.: On generic context lemmas for higher-order calculi with sharing. Theor. Comput. Sci. 411(11–13), 1521–1541 (2010)MATHCrossRefGoogle Scholar
  44. 44.
    Schmidt-Schauß, M., Sabel, D.: A Termination Proof of Reduction in a Simply Typed Calculus with Constructors. Frank report 42, Inst. für Informatik. Goethe-Universität Frankfurt (2010)Google Scholar
  45. 45.
    Schröder, L., Mossakowski, T.: HasCasl: integrated higher-order specification and program development. Theor. Comput. Sci. 410(12–13), 1217–1260 (2009)MATHCrossRefGoogle Scholar
  46. 46.
    Scott, D.: A type-theoretical alternative to CUCH, ISWIM, OWHY. Theor. Comput. Sci. 121, 411–440 (1993)MATHCrossRefGoogle Scholar
  47. 47.
    VeriFun Website: (2011). Accessed 1 May 2012
  48. 48.
    Walther, C.: Mathematical induction. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A., Siekmann, J.H. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming, vol. 2, pp. 127–228. Oxford University Press (1994)Google Scholar
  49. 49.
    Walther, C., Schweitzer, S.: Reasoning about incompletely defined programs. In: Sutcliffe, G., Voronkov, A. (eds.) Proc. LPAR ’05. Lecture Notes in Comput. Sci., vol. 3835, pp. 427–442 (2005)Google Scholar

Copyright information

© Springer Science+Business Media B.V. 2012

Authors and Affiliations

  1. 1.Institut für InformatikGoethe-UniversitätFrankfurtGermany

Personalised recommendations