skip to main content
10.1145/1481848.1481853acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
research-article

Compositional reasoning and decidable checking for dependent contract types

Published: 20 January 2009 Publication History

Abstract

Simple type systems perform compositional reasoning in that the type of a term depends only on the types of its subterms, and not on their semantics. Contracts offer more expressive abstractions, but static contract checking systems typically violate those abstractions and base their reasoning directly upon the semantics of terms. Pragmatically, this noncompositionality makes the decidability of static checking unpredictable.
We first show how compositional reasoning may be restored using standard type-theoretic techniques, namely existential types and subtyping. Despite its compositional nature, our type system is exact, in that the type of a term can completely capture its semantics, hence demonstrating that precision and compositionality are compatible. We then address predictability of static checking for contract types by giving a type-checking algorithm for an important class of programs with contract predicates drawn from a decidable theory. Our algorithm relies crucially on the fact that the type of a term depends only the types of its subterms (which fall into the decidable theory) and not their semantics (which will not, in general).

References

[1]
M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Levy. Explicit substitution. In Symposium on Principles of Programming Languages, pages 31--46, 1990.
[2]
L. Augustsson. Cayenne -- a language with dependent types. In Proceedings of the ACM International Conference on Functional Programming, pages 239--250, 1998. ISBN 1-58113-024-4.
[3]
M. Blume and D. McAllester. Sound and complete models for contracts. Journal of Functional Programming, 16:375--414, July 2006.
[4]
K. B. Bruce, L. Cardelli, and B. C. Pierce. Comparing object encodings. Information and Computation, 155(1/2):108--133, 1999.
[5]
S. Cui, K. Donnelly, and H. Xi. ATS: A Language That Combines Programming with Theorem Proving. In Proceedings of the 5th International Workshop on Frontiers of Combining Systems, pages 310--320, Vienna, Austria, September 2005.
[6]
E. Denney. Refinement types for specification. In Proceedings of the IFIP International Conference on Programming Concepts and Methods, volume 125, pages 148--166. Chapman & Hall, 1998. ISBN 0-412-83760-9.
[7]
D. Dreyer, K. Crary, and R. Harper. A type system for higher-order modules. In Symposium on Principles of Programming Languages, pages 236--249, 2003.
[8]
R. B. Findler and M. Felleisen. Contracts for higher-order functions. In Proceedings of the International Conference on Functional Programming, pages 48--59, 2002.
[9]
C. Flanagan. Hybrid type checking. In Symposium on Principles of Programming Languages, pages 245--256, 2006.
[10]
T. Freeman and F. Pfenning. Refinement types for ML. In Conference on Programming Language Design and Implementation, pages 268--277, 1991.
[11]
J. Gronski, K. Knowles, A. Tomb, S. N. Freund, and C. Flanagan. Sage: Practical hybrid checking for expressive types and specifications. In Proceedings of the Workshop on Scheme and Functional Programming, pages 93--104, 2006.
[12]
D. Grossman. Existential types for imperative languages. In European Symposium on Programming, pages 85--120, 2002.
[13]
R. Harper and M. Lillibridge. A type theoretic approach to higher-order modules with sharing. In Proceedings of the ACM Symposium on Principles of Programming Languages, pages 123--137, 1994.
[14]
K. Knowles and C. Flanagan. Type reconstruction for general refinement types. In European Symposium on Programming, 2007.
[15]
The Coq development team. The Coq proof assistant reference manual. LogiCal Project, 2004. URL http://coq.inria.fr. Version 8.0.
[16]
McBride. Faking it: Simulating dependent types in haskell. Journal of Functional Programming, 12(4-5):375--392, 2002.
[17]
C. McBride and J. McKinna. The view from the left. Journal of Functional Programming, 14(1):69--111, 2004.
[18]
J. C. Mitchell and G. D. Plotkin. Abstract types have existential type. Transactions on Programming Languages, 10(3):470--502, 1988.
[19]
G. Morrisett, D. Walker, K. Crary, and N. Glew. From System F to typed assembly language. ACM Transactions on Programming Languages and Systems, 21(3):527--568, 1999.
[20]
A. Nanevski, G. Morrisett, and L. Birkedal. Polymorphism and separation in hoare type theory. In International Conference on Functional Programming, pages 62--73, 2006.
[21]
U. Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 Göteborg, Sweden, September 2007.
[22]
X. Ou, G. Tan, Y. Mandelbaum, and D. Walker. Dynamic typing with dependent types. In Proceedings of the IFIP International Conference on Theoretical Computer Science, pages 437--450, 2004.
[23]
J. Rushby, S. Owre, and N. Shankar. Subtypes for specifications: predicate subtyping in PVS. IEEE Transactions on Software Engineering, 24(9): 709--720, 1998.
[24]
T. Sheard. Putting curry-howard to work. In Proceedings of the workshop on Haskell, pages 74--85, 2005.
[25]
C. A. Stone and R. Harper. Deciding type equivalence in a language with singleton kinds. In Symposium on Principles of Programming Languages, pages 214--227, 2000.
[26]
H. Xi and F. Pfenning. Dependent types in practical programming. In POPL '99: 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 214--227. ACM Press, 1999.
[27]
D. N. Xu. Extended static checking for haskell. In Proceedings of the workshop on Haskell, pages 48--59, 2006.
[28]
D. N. Xu, S. P. Jones, and K. Claessen. Static contract checking for haskell. In Draft Proceedings of the International Symposium on Implementation and Application of Functional Languages, pages 382--399, 2007.
[29]
C. Zenger. Indexed types. Theoretical Computer Science, 187(1-2):147--165, 1997.

Cited By

View all
  • (2024)Refinement Types for VisualizationProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695550(1871-1881)Online publication date: 27-Oct-2024
  • (2024)Mechanizing Refinement TypesProceedings of the ACM on Programming Languages10.1145/36329128:POPL(2099-2128)Online publication date: 5-Jan-2024
  • (2023)A Dependently Typed Language with Dynamic EqualityProceedings of the 8th ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3609027.3609407(44-57)Online publication date: 30-Aug-2023
  • Show More Cited By

Index Terms

  1. Compositional reasoning and decidable checking for dependent contract types

    Recommendations

    Comments

    Information & Contributors

    Information

    Published In

    cover image ACM Conferences
    PLPV '09: Proceedings of the 3rd workshop on Programming languages meets program verification
    January 2009
    90 pages
    ISBN:9781605583303
    DOI:10.1145/1481848
    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 January 2009

    Permissions

    Request permissions for this article.

    Check for updates

    Author Tags

    1. abstraction
    2. compositional reasoning
    3. dependent types
    4. refinement types

    Qualifiers

    • Research-article

    Conference

    POPL09
    Sponsor:

    Acceptance Rates

    Overall Acceptance Rate 18 of 25 submissions, 72%

    Upcoming Conference

    POPL '26

    Contributors

    Other Metrics

    Bibliometrics & Citations

    Bibliometrics

    Article Metrics

    • Downloads (Last 12 months)10
    • Downloads (Last 6 weeks)0
    Reflects downloads up to 22 Feb 2025

    Other Metrics

    Citations

    Cited By

    View all
    • (2024)Refinement Types for VisualizationProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695550(1871-1881)Online publication date: 27-Oct-2024
    • (2024)Mechanizing Refinement TypesProceedings of the ACM on Programming Languages10.1145/36329128:POPL(2099-2128)Online publication date: 5-Jan-2024
    • (2023)A Dependently Typed Language with Dynamic EqualityProceedings of the 8th ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3609027.3609407(44-57)Online publication date: 30-Aug-2023
    • (2022)Type-directed synthesis of visualizations from natural language queriesProceedings of the ACM on Programming Languages10.1145/35633076:OOPSLA2(532-559)Online publication date: 31-Oct-2022
    • (2022)A Hoare logic style refinement types formalisationProceedings of the 7th ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3546196.3550162(1-14)Online publication date: 6-Sep-2022
    • (2022)Revisiting occurrence typingScience of Computer Programming10.1016/j.scico.2022.102781217:COnline publication date: 1-May-2022
    • (2021)A General Semantic Construction of Dependent Refinement Type Systems, CategoricallyFoundations of Software Science and Computation Structures10.1007/978-3-030-71995-1_21(406-426)Online publication date: 23-Mar-2021
    • (2019)Resource-guided program synthesisProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3314221.3314602(253-268)Online publication date: 8-Jun-2019
    • (2017)Local refinement typingProceedings of the ACM on Programming Languages10.1145/31102701:ICFP(1-27)Online publication date: 29-Aug-2017
    • (2017)Stateful manifest contractsACM SIGPLAN Notices10.1145/3093333.300987552:1(530-544)Online publication date: 1-Jan-2017
    • 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