A language-based approach to functionally correct imperative programming

ABSTRACT

In this paper a language-based approach to functionally correct imperative programming is proposed. The approach is based on a programming language called RSP1, which combines dependent types, general recursion, and imperative features in a type-safe way, while preserving decidability of type checking. The methodology used is that of internal verification, where programs manipulate programmer-supplied proofs explicitly as data. The fundamental technical idea of RSP1 is to identify problematic operations as impure, and keep them out of dependent types. The resulting language is powerful enough to verify statically non-trivial properties of imperative and functional programs. The paper presents the ideas through the examples of statically verified merge sort, statically verified imperative binary search trees, and statically verified directed acyclic graphs.

REFERENCES

• 1: T. Altenkirch. Integrated verification in Type Theory. Lecture notes for a course at ESSLLI 96, Prague, 1996. available from the author's website.
• 2: Andrew W. Appel , Amy P. Felty, Dependent types ensure partial correctness of theorem provers, Journal of Functional Programming, v.14 n.1, p.3-19, January 2004 [doi>10.1017/S0956796803004921]
• 3: Lennart Augustsson, Cayenne—a language with dependent types, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.239-250, September 26-29, 1998, Baltimore, Maryland, United States
• 4: Franz Baader , Tobias Nipkow, Term rewriting and all that, Cambridge University Press, New York, NY, 1998
• 5: J. Brandt. What a Mesh: Dependent Data Types for Correct Mesh Manipulation Algorithms. Master's thesis, Washington University in Saint Louis, 2005. In preparation.
• 6: Chiyan Chen , Hongwei Xi, Combining programming with theorem proving, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 7: R. L. Constable , S. F. Allen , H. M. Bromley , W. R. Cleaveland , J. F. Cremer , R. W. Harper , D. J. Howe , T. B. Knoblock , N. P. Mendler , P. Panangaden , J. T. Sasaki , S. F. Smith, Implementing mathematics with the Nuprl proof development system, Prentice-Hall, Inc., Upper Saddle River, NJ, 1986
• 8: Thierry Coquand , Gerard Huet, The calculus of constructions, Information and Computation, v.76 n.2-3, p.95-120, February/March 1988 [doi>10.1016/0890-5401(88)90005-3]
• 9: G. Dowek, A. Felty, H. Herbelin, and G. Huet. The Coq proof assistant user's guide. Technical Report 154, Inria-Rocquencourt, France, 1993.
• 10: Healfdene Goguen, A syntactic approach to eta equality in type theory, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.75-84, January 12-14, 2005, Long Beach, California, USA
• 11: Robert Harper , Furio Honsell , Gordon Plotkin, A framework for defining logics, Journal of the ACM (JACM), v.40 n.1, p.143-184, Jan. 1993 [doi>10.1145/138027.138060]
• 12: Robert Harper , Frank Pfenning, On equivalence and canonical forms in the LF type theory, ACM Transactions on Computational Logic (TOCL), v.6 n.1, p.61-101, January 2005 [doi>10.1145/1042038.1042041]
• 13: R. Klapper and A. Stump. Validated Proof-Producing Decision Procedures. In C. Tinelli and S. Ranise, editors, 2nd International Workshop on Pragmatics of Decision Procedures in Automated Reasoning, 2004.
• 14: Nils Klarlund , Michael I. Schwartzbach, Graph types, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.196-205, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158628]
• 15: Z. Luo and R. Pollack. LEGO Proof Development System: User's Manual. Technical Report ECS-LFCS-92--211, Edinburgh LFCS, 1992.
• 16: Conor McBride , James McKinna, The view from the left, Journal of Functional Programming, v.14 n.1, p.69-111, January 2004 [doi>10.1017/S0956796803004829]
• 17: F. Mehta and T. Nipkow. Proving Pointer Programs in Higher-Order Logic. In F. Baader, editor, 19th International Conference on Automated Deduction, volume 2741 of LNCS, pages 121--135. Springer-Verlag, 2003.
• 18: Anders Møller , Michael I. Schwartzbach, The pointer assertion logic engine, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.221-231, June 2001, Snowbird, Utah, United States
• 19: B. Nordström, K. Petersson, and J. Smith. Programming in Martin-Löf's Type Theory. Oxford University Press, 1990.
• 20: Frank Pfenning, Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, p.221, June 16-19, 2001
• 21: F. Pfenning , C. Elliot, Higher-order abstract syntax, Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation, p.199-208, June 20-24, 1988, Atlanta, Georgia, United States
• 22: Frank Pfenning , Carsten Schürmann, System Description: Twelf - A Meta-Logical Framework for Deductive Systems, Proceedings of the 16th International Conference on Automated Deduction: Automated Deduction, p.202-206, July 07-10, 1999
• 23: Benjamin C. Pierce, Types and programming languages, MIT Press, Cambridge, MA, 2002
• 24: Benjamin C. Pierce , David N. Turner, Local type inference, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.252-265, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268967]
• 25: R. Pollack. Dependently typed records in type theory. Formal Aspects of Computing, 13:386--402, 2002.
• 26: John C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.55-74, July 22-25, 2002
• 27: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Parametric shape analysis via 3-valued logic, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.105-118, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292552]
• 28: J. Sarnat. LF-Sigma: The Metatheory of LF with Sigma types. Technical Report 1268, Yale CS department, 2004.
• 29: C. Schürmann and F. Pfenning. A Coverage Checking Algorithm for LF. In D. Basin and B. Wolff, editors, Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics, volume 2758 of LNCS, pages 120--135. Springer-Verlag, 2003.
• 30: E. Westbrook, A. Stump, and I. Wehrman. A Language-based Approach to Functionally Correct Imperative Programming. Technical Report WUCSE-2005-32, Washington University in Saint Louis, July 2005.
• 31: H. Xi. Facilitating Program Verification with Dependent Types. In Proceedings of the International Conference on Software Engineering and Formal Methods, pages 72--81, 2003.
• 32: D. Zhu and H. Xi. Safe Programming with Pointers through Stateful Views. In Proceedings of the 7th International Symposium on Practical Aspects of Declarative Languages, pages 83--97, Long Beach, CA, January 2005. Springer-Verlag LNCS vol. 3350.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

General Terms:
Languages, Verification

Keywords:
RSP, RSP1, dependent types, program verification