skip to main content
10.1145/1411204.1411237acmconferencesArticle/Chapter ViewAbstractPublication PagesicfpConference Proceedingsconference-collections
research-article

Ynot: dependent types for imperative programs

Published: 20 September 2008 Publication History

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.

Supplementary Material

JPG File (1411237.jpg)
index.html (index.html)
Slides from the presentation
ZIP File (p229-slides.zip)
Supplemental material for: Ynot: dependent types for imperative programs
Audio only (1411237.mp3)
Video (1411237.mp4)

References

[1]
R.-J. Back and J. von Wright. Refinement Calculus: A Systematic Introduction. Springer-Verlag, 1998. Graduate Texts in Computer Science.
[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]
N. Benton and A. Kennedy. Exceptional syntax. Journal of Functional Programming, 11(4):395--410, July 2001.
[4]
N. Benton and U. Zarfaty. Formalizing and verifying semantic type soundness for a simple compiler. In International Conference on Principles and Practice of Declarative Programming, PPDP'07, pages 1--12, 2007.
[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]
L. Burdy, Y. Cheon, D. Cok, M. Ernst, J. Kiniry, G. T. Leavens, K. R. M. Leino, and E. Poll. An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer, 7(3):212--232, June 2005.
[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]
E. W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM, 18(8):453--457, 1975.
[12]
X. Feng, Z. Shao, Y. Dong, and Y. Guo. Certifying low-level programs with hardware interrupts and preemptive threads. In Conference on Programming Language Design and Implementation, PLDI'08, pages 170--182, 2008.
[13]
J.-C. Filliâtre. Verification of non-functional programs using interpretations in type theory. Journal of Functional Programming, 13(4):709--745, July 2003.
[14]
C. Flanagan. Hybrid type checking. In Symposium on Principles of Programming Languages, POPL'06, pages 245--256, 2006.
[15]
S. Fogarty, E. Pasalic, J. Siek, and W. Taha. Concoqtion: Indexed types now! In Workshop on Partial Evaluation and Semantics-Based Program Manipulation, PEPM'07, 2007.
[16]
D. K. Gifford and J. M. Lucassen. Integrating functional and imperative programming. In Conference on LISP and Functional Programming, pages 28--38, 1986.
[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]
K. Honda, N. Yoshida, and M. Berger. An observationally complete program logic for imperative higher-order functions. In Symposium on Logic in Computer Science, LICS'05, pages 270--279, 2005.
[21]
T. Jim, G. Morrisett, D. Grossman, M. Hicks, J. Cheney, and Y. Wang. Cyclone: A safe dialect of C. In USENIX Annual Technical Conference, USENIX'02, pages 275--288, Monterey, Canada, 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]
T. Kleymann. Metatheory of verification calculi in LEGO: To what extent does syntax matter? In Types for Proofs and Programs, volume 1657 of Lecture Notes in Computer Science, pages 133--149, 1999.
[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. R. M. Leino and G. Nelson. Data abstraction and information hiding. ACM Transactions on Programming Languages and Systems, 24(5):491--553, 2002.
[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]
X. Leroy. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In Symposium on Principles of Programming Languages, POPL'06, pages 42--54, 2006.
[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. In Symposium on Logic in Computer Science, LICS'89, pages 14--23, Asilomar, California, 1989.
[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]
A. Nanevski, G. Morrisett, and L. Birkedal. Polymorphism and separation in Hoare Type Theory. In International Conference on Functional Programming, ICFP'06, pages 62--73, Portland, Oregon, 2006.
[34]
G. C. Necula. Proof-carrying code. In Symposium on Principles of Programming Languages, POPL'97, pages 106--119, Paris, January 1997.
[35]
Z. Ni and Z. Shao. Certified assembly programming with embedded code pointers. In Symposium on Principles of Programming Languages, POPL'06, pages 320--333, Charleston, South Carolina, January 2006.
[36]
P. O'Hearn, J. Reynolds, and H. Yang. Local reasoning about programs that alter data structures. In International Workshop on Computer Science Logic, CSL'01, volume 2142 of Lecture Notes in Computer Science, pages 1--19. Springer, 2001.
[37]
P. W. O'Hearn, H. Yang, and J. C. Reynolds. Separation and information hiding. In Symposium on Principles of Programming Languages, POPL'04, pages 268--280, 2004.
[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]
P. Rondon, M. Kawaguchi, and R. Jhala. Liquid types. In Conference on Programming Language Design and Implementation, PLDI'08, pages 159--169, 2008.
[41]
Z. Shao, V. Trifonov, B. Saha, and N. Papaspyrou. A type system for certified binaries. ACM Transactions on Programming Languages and Systems, 27(1):1--45, January 2005.
[42]
T. Sheard. Languages of the future. In International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA'04, pages 116--119, 2004.
[43]
M. Sozeau. Program-ing finger trees in Coq. In International Conference on Functional Programming, ICFP'07, pages 13--24, 2007.
[44]
W. Swierstra and T. Altenkirch. Beauty in the beast: A functional semantics of the awkward squad. In Haskell '07: Proceedings of the ACM SIGPLAN Workshop on Haskell, pages 25--36, 2007.
[45]
C. Varming and L. Birkedal. Higher-order separation logic in Isabelle/HOLCF. In Submitted for publication, 2008.
[46]
P. Wadler. The marriage of effects and monads. In International Conference on Functional Programming, ICFP'98, pages 63--74, Baltimore, Maryland, 1998.
[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]
E. Westbrook, A. Stump, and I. Wehrman. A language-based approach to functionally correct imperative programming. In International Conference on Functional Programming, ICFP'05, pages 268--279, 2005.
[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]
H. Xi and F. Pfenning. Eliminating array bound checking through dependent types. In Conference on Programming Language Design and Implementation, PLDI'98, pages 249--257, Montreal, Canada, 1998.

Cited By

View all
  • (2025)Formal Verification of Just-in-Time CompilationundefinedOnline publication date: 28-Jan-2025
  • (2024)Formal Verification of Data Modifications in Cloud Block Storage Based on Separation LogicChinese Journal of Electronics10.23919/cje.2022.00.11633:1(112-127)Online publication date: Jan-2024
  • (2024)A HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite AutomataProceedings of the ACM on Programming Languages10.1145/36564338:PLDI(1387-1411)Online publication date: 20-Jun-2024
  • Show More Cited By

Index Terms

  1. Ynot: dependent types for imperative programs

      Recommendations

      Comments

      Information & Contributors

      Information

      Published In

      cover image ACM Conferences
      ICFP '08: Proceedings of the 13th ACM SIGPLAN international conference on Functional programming
      September 2008
      422 pages
      ISBN:9781595939197
      DOI:10.1145/1411204
      • cover image ACM SIGPLAN Notices
        ACM SIGPLAN Notices  Volume 43, Issue 9
        ICFP '08
        September 2008
        399 pages
        ISSN:0362-1340
        EISSN:1558-1160
        DOI:10.1145/1411203
        Issue’s Table of Contents
      Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

      Sponsors

      Publisher

      Association for Computing Machinery

      New York, NY, United States

      Publication History

      Published: 20 September 2008

      Permissions

      Request permissions for this article.

      Check for updates

      Author Tags

      1. Hoare logic
      2. monads
      3. separation logic
      4. type theory

      Qualifiers

      • Research-article

      Conference

      ICFP08
      Sponsor:

      Acceptance Rates

      Overall Acceptance Rate 333 of 1,064 submissions, 31%

      Upcoming Conference

      ICFP '25
      ACM SIGPLAN International Conference on Functional Programming
      October 12 - 18, 2025
      Singapore , Singapore

      Contributors

      Other Metrics

      Bibliometrics & Citations

      Bibliometrics

      Article Metrics

      • Downloads (Last 12 months)38
      • Downloads (Last 6 weeks)1
      Reflects downloads up to 18 Feb 2025

      Other Metrics

      Citations

      Cited By

      View all
      • (2025)Formal Verification of Just-in-Time CompilationundefinedOnline publication date: 28-Jan-2025
      • (2024)Formal Verification of Data Modifications in Cloud Block Storage Based on Separation LogicChinese Journal of Electronics10.23919/cje.2022.00.11633:1(112-127)Online publication date: Jan-2024
      • (2024)A HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite AutomataProceedings of the ACM on Programming Languages10.1145/36564338:PLDI(1387-1411)Online publication date: 20-Jun-2024
      • (2024)Verifying Programs with Logic and Extended Proof Rules: Deep Embedding vs. Shallow EmbeddingJournal of Automated Reasoning10.1007/s10817-024-09706-568:3Online publication date: 10-Aug-2024
      • (2022)Specification-guided component-based synthesis from effectful librariesProceedings of the ACM on Programming Languages10.1145/35633106:OOPSLA2(616-645)Online publication date: 31-Oct-2022
      • (2022)Dependently-typed data plane programmingProceedings of the ACM on Programming Languages10.1145/34987016:POPL(1-28)Online publication date: 12-Jan-2022
      • (2021)Quantum Hoare Type Theory: Extended AbstractElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.340.15340(291-302)Online publication date: 6-Sep-2021
      • (2021)SMLtoCoq: Automated Generation of Coq Specifications and Proof Obligations from SML Programs with ContractsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.337.6337(71-87)Online publication date: 16-Jul-2021
      • (2021)How statically-typed functional programmers write codeProceedings of the ACM on Programming Languages10.1145/34855325:OOPSLA(1-30)Online publication date: 15-Oct-2021
      • (2021)Modular specification and verification of closures in RustProceedings of the ACM on Programming Languages10.1145/34855225:OOPSLA(1-29)Online publication date: 15-Oct-2021
      • Show More Cited By

      View Options

      Login options

      View options

      PDF

      View or Download as a PDF file.

      PDF

      eReader

      View online with eReader.

      eReader

      Figures

      Tables

      Media

      Share

      Share

      Share this Publication link

      Share on social media