×

Polymorphic contracts. (English) Zbl 1326.68077

Barthe, Gilles (ed.), Programming languages and systems. 20th European symposium on programming, ESOP 2011, held as part of the joint European conferences on theory and practice of software, ETAPS 2011, Saarbrücken, Germany, March 26 – April 3, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-19717-8/pbk). Lecture Notes in Computer Science 6602, 18-37 (2011).
Summary: Manifest contracts track precise properties by refining types with predicates – e.g., \(\{x : \text{Int} \mid x > 0 \}\) denotes the positive integers. Contracts and polymorphism make a natural combination: programmers can give strong contracts to abstract types, precisely stating pre- and post-conditions while hiding implementation details – for example, an abstract type of stacks might specify that the pop operation has input type \(\{x :\alpha\) Stack \(\mid \text{not}(\text{empty}x )\}\) . We formalize this combination by defining \(F_{H}\), a polymorphic calculus with manifest contracts, and establishing fundamental properties including type soundness and relational parametricity. Our development relies on a significant technical improvement over earlier presentations of contracts: instead of introducing a denotational model to break a problematic circularity between typing, subtyping, and evaluation, we develop the metatheory of contracts in a completely syntactic fashion, omitting subtyping from the core system and recovering it post facto as a derived property.
For the entire collection see [Zbl 1213.68027].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] PLT Racket Contracts, http://pre.plt-scheme.org/docs/html/guide/contracts.html
[2] Ahmed, A., Findler, R.B., Matthews, J., Wadler, P.: Blame for all. In: Workshop on Script-to-Program Evolution, STOP (2009) · doi:10.1145/1570506.1570507
[3] Ahmed, A., Findler, R.B., Siek, J., Wadler, P.: Blame for all. In: Principles of Programming Languages, POPL (2011) · Zbl 1284.68156 · doi:10.1145/1926385.1926409
[4] Aspinall, D., Compagnoni, A.: Subtyping dependent types. Theor. Comput. Sci. 266(1-2), 273–309 (2001) · Zbl 0989.68020 · doi:10.1016/S0304-3975(00)00175-4
[5] Findler, R.B., Felleisen, M.: Contracts for higher-order functions. In: International Conference on Functional Programming (ICFP), pp. 48–59 (2002) · Zbl 1322.68039 · doi:10.1145/581478.581484
[6] Flanagan, C.: Hybrid type checking. In: POPL, pp. 245–256 (2006) · Zbl 1370.68202 · doi:10.1145/1111037.1111059
[7] Greenberg, M., Pierce, B.C., Weirich, S.: Contracts made manifest. In: Principles of Programming Languages, POPL 2010 (2010) · Zbl 1312.68133 · doi:10.1145/1706299.1706341
[8] Gronski, J., Flanagan, C.: Unifying hybrid types and contracts. In: Trends in Functional Programming, TFP (2007)
[9] Guha, A., Matthews, J., Findler, R.B., Krishnamurthi, S.: Relationally-parametric polymorphic contracts. In: DLS, pp. 29–40 (2007) · doi:10.1145/1297081.1297089
[10] Knowles, K., Flanagan, C.: Hybrid type checking (2010) (to appear in TOPLAS) · Zbl 1187.68154
[11] Matthews, J., Ahmed, A.: Parametric polymorphism through run-time sealing or, theorems for low, low prices! In: Gairing, M. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 16–31. Springer, Heidelberg (2008) · Zbl 1133.68320 · doi:10.1007/978-3-540-78739-6_2
[12] Ou, X., Tan, G., Mandelbaum, Y., Walker, D.: Dynamic typing with dependent types. In: IFIP TCS, pp. 437–450 (2004) · Zbl 1088.68531 · doi:10.1007/1-4020-8141-3_34
[13] Pierce, B., Sumii, E.: Relating cryptography and polymorphism (July 2000)
[14] Pitts, A.M.: Typed operational reasoning. In: Pierce, B.C. (ed.) Advanced Topics in Types and Programming Languages, ch. 7, pp. 245–289. MIT Press, Cambridge (2005)
[15] Siek, J.G., Taha, W.: Gradual typing for functional languages. In: Scheme and Functional Programming Workshop (September 2006)
[16] Strickland, T.S., Tobin-Hochstadt, S., Felleisen, M.: Practical variable-arity polymorphism. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 32–46. Springer, Heidelberg (2009) · Zbl 1234.68061 · doi:10.1007/978-3-642-00590-9_3
[17] Wadler, P.: Theorems for free! In: Proceedings of ACM Conference on Functional Programming and Computer Architecture (FPCA 1989), pp. 347–359, London, UK (September 1989) · doi:10.1145/99370.99404
[18] Wadler, P., Findler, R.B.: Well-typed programs can’t be blamed. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 1–16. Springer, Heidelberg (2009) · Zbl 1234.68063 · doi:10.1007/978-3-642-00590-9_1
[19] Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation 115, 38–94 (1992) · Zbl 0938.68559 · doi:10.1006/inco.1994.1093
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.