skip to main content
research-article

Blame assignment for higher-order contracts with intersection and union

Published:29 August 2015Publication History
Skip Abstract Section

Abstract

We present an untyped calculus of blame assignment for a higher-order contract system with two new operators: intersection and union. The specification of these operators is based on the corresponding type theoretic constructions. This connection makes intersection and union contracts their inevitable dynamic counterparts with a range of desirable properties and makes them suitable for subsequent integration in a gradual type system. A denotational specification provides the semantics of a contract in terms of two sets: a set of terms satisfying the contract and a set of contexts respecting the contract. This kind of specification for contracts is novel and interesting in its own right. A nondeterministic operational semantics serves as the specification for contract monitoring and for proving its correctness. It is complemented by a deterministic semantics that is closer to an implementation and that is connected to the nondeterministic semantics by simulation. The calculus is the formal basis of TJS, a language embedded, higher-order contract system implemented for JavaScript.

References

  1. A. Ahmed, R. B. Findler, J. G. Siek, and P. Wadler. Blame for all. In T. Ball and M. Sagiv, editors, Proc. 38th ACM Symp. POPL, pages 201–214, Austin, TX, USA, Jan. 2011. ACM Press. Google ScholarGoogle ScholarDigital LibraryDigital Library
  2. F. Barbanera and M. Dezani-Ciancaglini. Intersection and union types. In T. Ito and A. Meyer, editors, Proc. Theoretical Aspects of Computer Software, volume 526 of LNCS, Sendai, Japan, 1991. Springer. Google ScholarGoogle ScholarDigital LibraryDigital Library
  3. F. Barbanera, M. Dezani-Ciancaglini, and U. de’ Liguoro. Intersection and union types: Syntax and semantics. Information and Computation, 119(2):202–230, 1995. Google ScholarGoogle ScholarDigital LibraryDigital Library
  4. M. Blume and D. McAllester. Sound and complete models of contracts. J. Funct. Program., 16:375–414, July 2006. Google ScholarGoogle ScholarDigital LibraryDigital Library
  5. M. Coppo and M. Dezani-Ciancaglini. A new type-assignment for λ-terms. Archiv. Math. Logik, 19(139-156), 1978.Google ScholarGoogle Scholar
  6. R. Davies and F. Pfenning. Intersection types and computational effects. In P. Wadler, editor, Proc. ICFP 2000, pages 198–208, Montreal, Canada, Sept. 2000. ACM Press, New York. Google ScholarGoogle ScholarDigital LibraryDigital Library
  7. C. Dimoulas and M. Felleisen. On contract satisfaction in a higher-order world. ACM TOPLAS, 33(5):16, 2011. Google ScholarGoogle ScholarDigital LibraryDigital Library
  8. C. Dimoulas, R. B. Findler, C. Flanagan, and M. Felleisen. Correct blame for contracts: No more scapegoating. In T. Ball and M. Sagiv, editors, Proc. 38th ACM Symp. POPL, pages 215–226, Austin, TX, USA, Jan. 2011. ACM Press. Google ScholarGoogle ScholarDigital LibraryDigital Library
  9. T. Disney, C. Flanagan, and J. McCarthy. Temporal higher-order contracts. In O. Danvy, editor, Proc. ICFP 2011, pages 176–188, Tokyo, Japan, Sept. 2011. ACM Press, New York. Google ScholarGoogle ScholarDigital LibraryDigital Library
  10. J. Dunfield and F. Pfenning. Type assignment for intersections and unions in call-by-value languages. In A. D. Gordon, editor, FOSSACS 2003, volume 2620 of LNCS, pages 250–266. Springer, 2003. Google ScholarGoogle ScholarDigital LibraryDigital Library
  11. R. B. Findler and M. Blume. Contracts as pairs of projections. In P. Wadler and M. Hagiya, editors, Proceedings of the 8th International Symposium on Functional and Logic Programming FLOPS 2006, pages 226–241, Fuji Susono, Japan, Apr. 2006. Springer. Google ScholarGoogle ScholarDigital LibraryDigital Library
  12. R. B. Findler, M. Blume, and M. Felleisen. An investigation of contracts as projections. Technical Report TR-2004-02, University of Chicago, Computer Science Department, 2004.Google ScholarGoogle Scholar
  13. R. B. Findler and M. Felleisen. Contracts for higher-order functions. In S. Peyton-Jones, editor, Proc. ICFP 2002, pages 48–59, Pittsburgh, PA, USA, Oct. 2002. ACM Press, New York. Google ScholarGoogle ScholarDigital LibraryDigital Library
  14. M. Flatt and PLT. The Racket Reference, v.6.1.1 edition, 2015. http://docs.racket-lang.org/reference/index.html.Google ScholarGoogle Scholar
  15. R. Floyd. Assigning meanings to programs. In Proceedings of Symposia in Applied Mathematics, pages 19–32, 1967.Google ScholarGoogle Scholar
  16. M. Furr, J. An, J. S. Foster, and M. W. Hicks. Static type inference for Ruby. In S. Y. Shin and S. Ossowski, editors, SAC, pages 1859–1866, Honolulu, Hawaii, USA, Mar. 2009. ACM. Google ScholarGoogle ScholarDigital LibraryDigital Library
  17. A. Guha, J. Matthews, R. B. Findler, and S. Krishnamurthi. Relationally-parametric polymorphic contracts. In P. Costanza and R. Hirschfeld, editors, DLS, pages 29–40. ACM, 2007. Google ScholarGoogle ScholarDigital LibraryDigital Library
  18. R. Hinze, J. Jeuring, and A. Löh. Typed contracts for functional programming. In P. Wadler and M. Hagiya, editors, Proceedings of the 8th International Symposium on Functional and Logic Programming FLOPS 2006, pages 208–225, Fuji Susono, Japan, Apr. 2006. Springer. Google ScholarGoogle ScholarDigital LibraryDigital Library
  19. C. A. R. Hoare. An axiomatic basis for computer programming. Comm. ACM, 12:576–580, 1969. Google ScholarGoogle ScholarDigital LibraryDigital Library
  20. H. Hosoya, J. Vouillon, and B. C. Pierce. Regular expression types for XML. ACM TOPLAS, 27(1), 2004. Google ScholarGoogle ScholarDigital LibraryDigital Library
  21. M. Keil and P. Thiemann. Blame assignment for higher-order contracts with intersection and union. Technical report, Institute for Computer Science, University of Freiburg, 2015.Google ScholarGoogle Scholar
  22. B. Meyer. Object-Oriented Software Construction. Prentice-Hall, 1988. Google ScholarGoogle ScholarDigital LibraryDigital Library
  23. B. Meyer. Object-Oriented Software Construction. Prentice-Hall, Upper Saddle River, NJ, USA, 2nd edition, 1997. Google ScholarGoogle ScholarDigital LibraryDigital Library
  24. B. Pierce. Programming with intersection types, union types, and polymorphism. Technical Report CMU-CS-91-106, Carnegie Mellon University, Feb. 1991.Google ScholarGoogle Scholar
  25. B. C. Pierce. Programming with Intersection Types and Bounded Polymorphism. PhD thesis, Carnegie Mellon University, Dec. 1991. Google ScholarGoogle ScholarDigital LibraryDigital Library
  26. J. G. Siek and W. Taha. Gradual typing for functional languages. In Scheme and Functional Programming Workshop, Sept. 2006.Google ScholarGoogle Scholar
  27. S. Tobin-Hochstadt and M. Felleisen. Interlanguage migration: From scripts to programs. In Dynamic Languages Symposium, DLS 2006, pages 964–974, Portland, Oregon, USA, 2006. ACM. Google ScholarGoogle ScholarDigital LibraryDigital Library
  28. S. Tobin-Hochstadt and M. Felleisen. The design and implementation of typed scheme. In P. Wadler, editor, Proc. 35th ACM Symp. POPL, pages 395–406, San Francisco, CA, USA, Jan. 2008. ACM Press. Google ScholarGoogle ScholarDigital LibraryDigital Library
  29. S. Tobin-Hochstadt and D. Van Horn. Higher-order symbolic execution via contracts. In G. T. Leavens and M. B. Dwyer, editors, OOPSLA, pages 537–554. ACM, 2012. Google ScholarGoogle ScholarDigital LibraryDigital Library
  30. J. A. Tov and R. Pucella. Stateful contracts for affine types. In A. D. Gordon, editor, ESOP 2010, volume 6012 of LNCS, pages 550–569. Springer, 2010. Google ScholarGoogle ScholarDigital LibraryDigital Library
  31. P. Wadler and R. B. Findler. Well-typed programs can’t be blamed. In Proc. 18th ESOP, volume 5502 of LNCS, pages 1–16, York, UK, Mar. 2009. Springer. Google ScholarGoogle ScholarDigital LibraryDigital Library
  32. A. K. Wright and R. Cartwright. A practical soft type system for Scheme. ACM TOPLAS, 19(1):87–152, Jan. 1997. Google ScholarGoogle ScholarDigital LibraryDigital Library

Index Terms

  1. Blame assignment for higher-order contracts with intersection and union

            Recommendations

            Comments

            Login options

            Check if you have access through your login credentials or your institution to get full access on this article.

            Sign in

            Full Access

            • Published in

              cover image ACM SIGPLAN Notices
              ACM SIGPLAN Notices  Volume 50, Issue 9
              ICFP '15
              September 2015
              436 pages
              ISSN:0362-1340
              EISSN:1558-1160
              DOI:10.1145/2858949
              • Editor:
              • Andy Gill
              Issue’s Table of Contents
              • cover image ACM Conferences
                ICFP 2015: Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming
                August 2015
                436 pages
                ISBN:9781450336697
                DOI:10.1145/2784731

              Copyright © 2015 ACM

              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]

              Publisher

              Association for Computing Machinery

              New York, NY, United States

              Publication History

              • Published: 29 August 2015

              Check for updates

              Qualifiers

              • research-article

            PDF Format

            View or Download as a PDF file.

            PDF

            eReader

            View online with eReader.

            eReader