Ynot: dependent types for imperative programs

ABSTRACT

We describe an axiomatic extension to the Coq proof assistant, that supports writing, reasoning about, and extracting higher-order, dependently-typed programs with side-effects. Coq already includes a powerful functional language that supports dependent types, but that language is limited to pure, total functions. The key contribution of our extension, which we call Ynot, is the added support for computations that may have effects such as non-termination, accessing a mutable store, and throwing/catching exceptions.

The axioms of Ynot form a small trusted computing base which has been formally justified in our previous work on Hoare Type Theory (HTT). We show how these axioms can be combined with the powerful type and abstraction mechanisms of Coq to build higher-level reasoning mechanisms which in turn can be used to build realistic, verified software components. To substantiate this claim, we describe here a representative series of modules that implement imperative finite maps, including support for a higher-order (effectful) iterator. The implementations range from simple (e.g., association lists) to complex (e.g., hash tables) but share a common interface which abstracts the implementation details and ensures that the modules properly implement the finite map abstraction.

REFERENCES

• 1: Ralph-Johan J. Back , Abo Akademi , J. Von Wright , F. B. Schneider , D. Gries, Refinement Calculus: A Systematic Introduction, Springer-Verlag New York, Inc., Secaucus, NJ, 1998
• 2: M. Barnett, K. R. M. Leino, andW. Schulte. The Spec# programming system: An overview. In International Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart Devices, CASSIS'04, volume 3362 of Lecture Notes in Computer Science. Springer, 2004.
• 3: Nick Benton , Andrew Kennedy, Exceptional syntax, Journal of Functional Programming, v.11 n.4, p.395-410, July 2001 [doi>10.1017/S0956796801004099]
• 4: Nick Benton , Uri Zarfaty, Formalizing and verifying semantic type soundness of a simple compiler, Proceedings of the 9th ACM SIGPLAN international conference on Principles and practice of declarative programming, July 14-16, 2007, Wroclaw, Poland [doi>10.1145/1273920.1273922]
• 5: L. Birkedal and H. Yang. Relational parametricity and separation logic. In FOSSACS'07, volume 4423 of LNCS, 2007.
• 6: S. Boulmé. Intuitionistic refinement calculus. In International Conference on Typed Lambda Calculus and Applications, TLCA'07, pages 54--69, 2007.
• 7: Lilian Burdy , Yoonsik Cheon , David R. Cok , Michael D. Ernst , Joseph R. Kiniry , Gary T. Leavens , K. Rustan M. Leino , Erik Poll, An overview of JML tools and applications, International Journal on Software Tools for Technology Transfer (STTT), v.7 n.3, p.212-232, June 2005 [doi>10.1007/s10009-004-0167-4]
• 8: J. Condit, M. Harren, Z. Anderson, D. Gay, and G. Necula. Dependent types for low-level programming. In European Symposium on Programming, ESOP'07, volume 4421 of Lecture Notes in Computer Science, pages 520--535. Springer, 2007.
• 9: L. Cruz-Filipe and P. Letouzey. A Large-Scale Experiment in Executing Extracted Programs. In Calculemus'05, 2005.
• 10: D. L. Detlefs, K. R. M. Leino, G. Nelson, and J. B. Saxe. Extended static checking. Compaq Systems Research Center, Research Report 159, December 1998.
• 11: Edsger W. Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, Communications of the ACM, v.18 n.8, p.453-457, Aug. 1975 [doi>10.1145/360933.360975]
• 12: Xinyu Feng , Zhong Shao , Yuan Dong , Yu Guo, Certifying low-level programs with hardware interrupts and preemptive threads, Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, June 07-13, 2008, Tucson, AZ, USA
• 13: Jean-Christophe Filliâtre, Verification of non-functional programs using interpretations in type theory, Journal of Functional Programming, v.13 n.4, p.709-745, July 2003 [doi>10.1017/S095679680200446X]
• 14: Cormac Flanagan, Hybrid type checking, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.245-256, January 11-13, 2006, Charleston, South Carolina, USA
• 15: Seth Fogarty , Emir Pasalic , Jeremy Siek , Walid Taha, Concoqtion: indexed types now!, Proceedings of the 2007 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 15-16, 2007, Nice, France [doi>10.1145/1244381.1244400]
• 16: David K. Gifford , John M. Lucassen, Integrating functional and imperative programming, Proceedings of the 1986 ACM conference on LISP and functional programming, p.28-38, August 1986, Cambridge, Massachusetts, United States [doi>10.1145/319838.319848]
• 17: G. Gonthier. A computer-checked proof of the Four Colour Theorem. http://research.microsoft.com/~gonthier/4colproof.pdf, 2005.
• 18: A. Hobor, A. W. Appel, and F. Z. Nardelli. Oracle semantics for concurrent separation logic. In European Symposium on Programming, ESOP'08, pages 353--367, 2008.
• 19: P. V. Homeier and D. F. Martin. A mechanically verified verification condition generator. The Computer Journal, 38(2):131--141, 1995.
• 20: An Observationally Complete Program Logic for Imperative Higher-Order Frame Rules, Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, p.260-279, June 26-29, 2005 [doi>10.1109/LICS.2005.5]
• 21: Trevor Jim , J. Greg Morrisett , Dan Grossman , Michael W. Hicks , James Cheney , Yanling Wang, Cyclone: A Safe Dialect of C, Proceedings of the General Track of the annual conference on USENIX Annual Technical Conference, p.275-288, June 10-15, 2002
• 22: C. B. Jones. Some mistakes I have made and what I have learned from them. In Fundamental Approaches to Software Engineering, volume 1382 of Lecture Notes in Computer Science, pages 7--20. Springer-Verlag, 1998.
• 23: Thomas Kleymann, Metatheory of Verification Calculi in LEGO - To what Extent Does Syntax Matter?, Selected papers from the International Workshop on Types for Proofs and Programs, p.133-148, March 27-31, 1998
• 24: N. R. Krishnaswami, L. Birkedal, and J. Aldrich. Modular verification of the subject-observer pattern via higher-order separation logic. Presented at the FTFJP 2007 workshop, 2007.
• 25: K. Rustan M. Leino , Greg Nelson, Data abstraction and information hiding, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.5, p.491-553, September 2002 [doi>10.1145/570886.570888]
• 26: K. R. M. Leino, G. Nelson, and J. B. Saxe. ESC/Java User's Manual. Compaq Systems Research Center, October 2000. Technical Note 2000-002.
• 27: Xavier Leroy, Formal certification of a compiler back-end or: programming a compiler with a proof assistant, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.42-54, January 11-13, 2006, Charleston, South Carolina, USA
• 28: P. Letouzey. A New Extraction for Coq. In H. Geuvers and F. Wiedijk, editors, Types for Proofs and Programs, Second International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, volume 2646 of Lecture Notes in Computer Science. Springer-Verlag, 2003.
• 29: N. Marti and R. Affeldt. A certified verifier for a fragment of Separation logic. In JSSST Workshop on Programming and Programming Languages (PPL'07). Japan Society for Software Science and Technology, 2007.
• 30: The Coq development team. The Coq proof assistant reference manual. LogiCal Project, 2004. Version 8.0.
• 31: E. Moggi, Computational lambda-calculus and monads, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.14-23, June 1989, Pacific Grove, California, United States
• 32: A. Nanevski, A. Ahmed, G. Morrisett, and L. Birkedal. Abstract Predicates and Mutable ADTs in Hoare Type Theory. In European Symposium on Programming, ESOP'07, volume 4421 of Lecture Notes in Computer Science, pages 189--204. Springer, 2007.
• 33: Aleksandar Nanevski , Greg Morrisett , Lars Birkedal, Polymorphism and separation in hoare type theory, Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, September 16-21, 2006, Portland, Oregon, USA
• 34: George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
• 35: Zhaozhong Ni , Zhong Shao, Certified assembly programming with embedded code pointers, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.320-333, January 11-13, 2006, Charleston, South Carolina, USA
• 36: Peter W. O'Hearn , John C. Reynolds , Hongseok Yang, Local Reasoning about Programs that Alter Data Structures, Proceedings of the 15th International Workshop on Computer Science Logic, p.1-19, September 10-13, 2001
• 37: Peter W. O'Hearn , Hongseok Yang , John C. Reynolds, Separation and information hiding, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.268-280, January 14-16, 2004, Venice, Italy
• 38: R. L. Petersen, L. Birkedal, A. Nanevski, and G. Morrisett. A realizability model for impredicative Hoare Type Theory. In European Symposium on Programming, ESOP'08, 2008.
• 39: V. Preoteasa. Mechanical verification of recursive procedures manipulating pointers using separation logic. In 14th International Symposium on Formal Methods, pages 508--523, August 2006.
• 40: Patrick M. Rondon , Ming Kawaguci , Ranjit Jhala, Liquid types, Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, June 07-13, 2008, Tucson, AZ, USA
• 41: Zhong Shao , Valery Trifonov , Bratin Saha , Nikolaos Papaspyrou, A type system for certified binaries, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.1, p.1-45, January 2005 [doi>10.1145/1053468.1053469]
• 42: Tim Sheard, Languages of the future, Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 24-28, 2004, Vancouver, BC, CANADA [doi>10.1145/1028664.1028711]
• 43: Matthieu Sozeau, Program-ing finger trees in Coq, Proceedings of the 12th ACM SIGPLAN international conference on Functional programming, October 01-03, 2007, Freiburg, Germany
• 44: Wouter Swierstra , Thorsten Altenkirch, Beauty in the beast, Proceedings of the ACM SIGPLAN workshop on Haskell workshop, September 30-30, 2007, Freiburg, Germany [doi>10.1145/1291201.1291206]
• 45: Carsten Varming , Lars Birkedal, Higher-Order Separation Logic in Isabelle/HOLCF, Electronic Notes in Theoretical Computer Science (ENTCS), 218, p.371-389, October, 2008 [doi>10.1016/j.entcs.2008.10.022]
• 46: Philip Wadler, The marriage of effects and monads, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.63-74, September 26-29, 1998, Baltimore, Maryland, United States
• 47: T. Weber. Towards mechanized program verification with separation logic. In Proceedings of CSL'04, volume 3210 of LNCS, pages 250--264. Springer, 2004.
• 48: Edwin Westbrook , Aaron Stump , Ian Wehrman, A language-based approach to functionally correct imperative programming, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 49: M. Wildmoser. Verified Proof Carrying Code. PhD thesis, Institut für Informatik, Technische Universität München, 2005.
• 50: M. Wildmoser and T. Nipkow. Certifying machine code safety: Shallow versus deep embedding. In Applications of Higher Order Logic Theorem Proving, TPHOL'04, volume 3223 of Lecture Notes in Computer Science, pages 305--320, 2004..
• 51: H. Xi. Applied Type System (extended abstract). In TYPES'03, pages 394--408. Springer-Verlag LNCS 3085, 2004.
• 52: Hongwei Xi , Frank Pfenning, Eliminating array bound checking through dependent types, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.249-257, June 17-19, 1998, Montreal, Quebec, Canada

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Languages, Verification

Keywords:
Hoare logic, monads, separation logic, type theory