Semantic subtyping with an SMT solver

ABSTRACT

We study a first-order functional language with the novel combination of the ideas of refinement type (the subset of a type to satisfy a Boolean expression) and type-test (a Boolean expression testing whether a value belongs to a type). Our core calculus can express a rich variety of typing idioms; for example, intersection, union, negation, singleton, nullable, variant, and algebraic types are all derivable. We formulate a semantics in which expressions denote terms, and types are interpreted as first-order logic formulas. Subtyping is defined as valid implication between the semantics of types. The formulas are interpreted in a specific model that we axiomatize using standard first-order theories. On this basis, we present a novel type-checking algorithm able to eliminate many dynamic tests and to detect many errors statically. The key idea is to rely on an SMT solver to compute subtyping efficiently. Moreover, interpreting types as formulas allows us to call the SMT solver at run-time to compute instances of types.

References

1. }}The Microsoft code name "M" Modeling Language Specification Version 0.5. Microsoft Corporation, Oct. 2009. Preliminary implementation available as part of the SQL Server Modeling CTP (November 2009).
2. }}A. Aiken and E. Wimmers. Type inclusion constraints and type inference. In Proceedings of ICFP, 1993.
3. }}D. Aspinall and M. Hofmann. Dependent types. In Advanced Topics in Types and Programming Languages, chapter 2. MIT Press, 2005.
4. }}C. Barrett, M. Deters, A. Oliveras, and A. Stump. Design and results of the 3rd Annual SMT Competition. International Journal on Artificial Intelligence Tools, 17(4):569--606, 2008.
5. }}C. Barrett and C. Tinelli. CVC3. In Proceedings of CAV, 2007.
6. }}J. Bengtson, K. Bhargavan, C. Fournet, A. D. Gordon, and S. Maffeis. Refinement types for secure implementations. In Proceedings of CSF, 2008.
7. }}V. Benzaken, G. Castagna, and A. Frisch. CDuce: An XML-friendly general purpose language. In Proceedings of ICFP, 2003.
8. }}G. M. Bierman, A. D. Gordon, C. Hriţcu, and D. Langworthy. Semantic subtyping with an SMT solver. Technical Report MSR--TR--2010--99, Microsoft Research, July 2010.
9. }}P. Buneman, S. Naqvi, V. Tannen, and L. Wong. Principles of programming with complex objects and collection types. Theoretical Computer Science, 149(1):3--48, 1995.
10. }}R. M. Burstall, D. B. MacQueen, and D. Sannella. HOPE: An experimental applicative language. In LISP Conference, pages 136--143, 1980.
11. }}D. Crockford. The application/json media type for JavaScript Object Notation (JSON), July 2006. RFC 4627.
12. }}F. Damm. Subtyping with union types, intersection types and recursive types. In Proceedings of TACS, 1994.
13. }}L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In Proceedings of TACAS, 2008.
14. }}L. M. de Moura and N. Bjørner. Generalized, efficient array decision procedures. In FMCAD, 2009.
15. }}D. Detlefs, G. Nelson, and J. B. Saxe. Simplify: a theorem prover for program checking. J. ACM, 52(3):365--473, 2005.
16. }}J. Dunfield and F. Pfenning. Tridirectional typechecking. In Proceedings of POPL, pages 281--292, 2004.
17. }}B. Dutertre and L. de Moura. The YICES SMT solver. Available at http://yices.csl.sri.com/tool-paper.pdf, 2006.
18. }}R. Findler and M. Felleisen. Contracts for higher-order functions. In ICFP, 2002.
19. }}K. Fisher, Y. Mandelbaum, and D. Walker. The next 700 data description languages. In Proceedings of POPL, 2006.
20. }}C. Flanagan. Hybrid type checking. In Proceedings of POPL, 2006.
21. }}T. Freeman and F. Pfenning. Refinement types for ML. In Proceedings of PLDI, 1991.
22. }}A. Frisch, G. Castagna, and V. Benzaken. Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types. J. ACM, 55(4), 2008.
23. }}A. D. Gordon and A. Jeffrey. Typing one-to-one and one-to-many correspondences in security protocols. In Proceedings of ISSS, 2002.
24. }}H. Hosoya, J. Vouillon, and B. Pierce. Regular expression types for XML. In Proceedings of ICFP, 2000.
25. }}C. Jones. Systematic software development using VDM. Prentice-Hall Englewood Cliffs, NJ, 1986.
26. }}K. Knowles, A. Tomb, J. Gronski, S. Freund, and C. Flanagan. Sage: Unified hybrid checking for first-class types, general refinement types and Dynamic. Technical report, UCSC, 2007.
27. }}A. Kopylov. Dependent intersection: A new way of defining records in type theory. In LICS, pages 86--95. IEEE Computer Society, 2003.
28. }}K. R. M. Leino and R. Monahan. Reasoning about comprehensions with first-order SMT solvers. In Proceedings of SAC, 2009.
29. }}W. Lovas and F. Pfenning. A bidirectional refinement type system for LF. In Proceedings of LFMTP, 2007.
30. }}E. Meijer, B. Beckman, and G. Bierman. LINQ: Reconciling objects, relations and XML in the .NET framework. In Proceedings of SIGMOD, 2007.
31. }}J. Meng and L. C. Paulson. Translating higher-order problems to first-order clauses. Journal of Automated Reasoning, 40(1):35--60, 2008.
32. }}B. Meyer. Eiffel: the language. Prentice Hall, 1992.
33. }}B. Nordström and K. Petersson. Types and specifications. In IFIP'83, 1983.
34. }}B. C. Pierce. Types and Programming Languages. MIT Press, 2002.
35. }}B. C. Pierce and D. N. Turner. Local type inference. In Proceedings of POPL, 1998.
36. }}S. Ranise and C. Tinelli. The SMT-LIB Standard: Version 1.2, 2006.
37. }}J. C. Reynolds. Design of the programming language Forsythe. In Algol-Like Languages, chapter 8. Birkhäser, 1996.
38. }}P. Rondon, M. Kawaguchi, and R. Jhala. Liquid types. In Proceedings of PLDI, 2008.
39. }}J. Rushby, S. Owre, and N. Shankar. Subtypes for specifications: Predicate subtyping in PVS. IEEE Transactions on Software Engineering, 24(9):709--720, 1998.
40. }}V. Saraswat, N. Nystrom, J. Palsberg, and C. Grothoff. Constrained types for object-oriented languages. In Proceedings of OOPSLA, 2008.
41. }}M. Sozeau. Subset coercions in Coq. In Proceedings of TYPES, 2006.
42. }}S. Tobin-Hochstadt and M. Felleisen. Logical types for Scheme. In Proceedings of ICFP, 2010.
43. }}H. Xi and F. Pfenning. Dependent types in practical programming. In Proceedings of POPL, 1999.

Index Terms

• Software and its engineering

  • Software notations and tools

    • Formal language definitions

      • Semantics

• Theory of computation

  • Semantics and reasoning

    • Program constructs

      • Type structures

    • Program reasoning

      • Program analysis

    • Program semantics

      • Denotational semantics

      • Operational semantics