Kenneth Knowles
Cormac Flanagan
Abstract
Traditional static type systems are effective for verifying basic interface specifications. Dynamically checked contracts support more precise specifications, but these are not checked until runtime, resulting in incomplete detection of defects. Hybrid type checking is a synthesis of these two approaches that enforces precise interface specifications, via static analysis where possible, but also via dynamic checks where necessary. This article explores the key ideas and implications of hybrid type checking, in the context of the λ-calculus extended with contract types, that is, with dependent function types and with arbitrary refinements of base types.
- Parnas, D. L. 1972. A technique for software module specification with examples. Comm. ACM 15, 5, 330--336. Google Scholar
Digital Library
- Abadi, M., Cardelli, L., Pierce, B., and Plotkin, G. 1989. Dynamic typing in a statically-typed language. In Proceedings of the Symposium on Principles of Programming Languages. 213--227. Google ScholarDigital Library
- Agarwal, R. and Stoller, S. D. 2004. Type inference for parameterized race-free Java. In Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation. 149--160.Google Scholar
- Aiken, A., Wimmers, E. L., and Lakshman, T. K. 1994. Soft typing with conditional types. In Proceedings of the Symposium on Principles of Programming Languages. 163--173. Google ScholarDigital Library
- Augustsson, L. 1998. Cayenne — A language with dependent types. In Proceedings of the ACM International Conference on Functional Programming. 239--250. Google ScholarDigital Library
- Blei, D., Harrelson, C., Jhala, R., Majumdar, R., Necula, G. C., Rahul, S. P., Weimer, W., and Weitz, D. 2000. Vampyre. http://www-cad.eecs.berkeley.edu/~rupak/Vampyre/.Google Scholar
- Blume, M. and McAllester, D. 2006. Sound and complete models for contracts. J. Funct. Program.16, 375--414. Google ScholarDigital Library
- Breazu-Tannen, V., Coquand, T., Gunter, C. A., and Scedrov, A. 1991. Inheritance as implicit coercion. Inform. Comput. 93, 1, 172--221. Google ScholarDigital Library
- Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G., Leino, K., and Poll, E. 2003. An overview of JML tools and applications. In 8th International Workshop on Formal Methods for Industrial Critical Systems (FMICS '03). Electronic Notes in Theoretical Computer Science, T. Arts and W. Fokkink, Eds., vol. 80. Elsevier. 73--89.Google Scholar
- Cardelli, L. 1988a. Phase distinctions in type theory. Manuscript. http://lucacardelli.name/Papers/PhaseDistinctions.pdf.Google Scholar
- Cardelli, L. 1988b. Typechecking dependent types and subtypes. In Foundations of Logic and Functional Programming. Lecture Notes in Computer Science. Springer, 45--57.Google ScholarDigital Library
- Davies, R. and Pfenning, F. 2000. Intersection types and computational effects. In Proceedings of the International Conference on Functional Programming. 198--208. Google ScholarDigital Library
- Denney, E. 1998. Refinement types for specification. In Proceedings of the IFIP International Conference on Programming Concepts and Methods. Vol. 125. Chapman and Hall, 148--166. Google ScholarDigital Library
- Detlefs, D., Nelson, G., and Saxe, J. B. 2005. Simplify: A theorem prover for program checking. J. ACM 52, 3, 365--473. Google ScholarDigital Library
- Fagan, M. 1990. Soft typing. Ph.D. thesis, Rice University.Google Scholar
- Findler, R. B. 2002. Behavioral software contracts. Ph.D. thesis, Rice University. Google ScholarDigital Library
- Findler, R. B. and Felleisen, M. 2002. Contracts for higher-order functions. In Proceedings of the International Conference on Functional Programming. 48--59. Google ScholarDigital Library
- Flanagan, C. 2006. Hybrid type checking. In Proceedings of the Symposium on Principles of Programming Languages. 245--256. Google ScholarDigital Library
- Flanagan, C., Flatt, M., Krishnamurthi, S., Weirich, S., and Felleisen, M. 1996. Finding bugs in the web of program invariants. In Proceedings of the Conference on Programming Language Design and Implementation. 23--32. Google ScholarDigital Library
- Flanagan, C., Leino, K. R. M., Lillibridge, M., Nelson, G., Saxe, J. B., and Stata, R. 2002. Extended static checking for Java. In Proceedings of the Conference on Programming Language Design and Implementation. 234--245. Google ScholarDigital Library
- Freeman, T. and Pfenning, F. 1991. Refinement types for ML. In Proceedings of the Conference on Programming Language Design and Implementation. 268--277. Google ScholarDigital Library
- Frisch, A., Castagna, G., and Benzaken, V. 2002. Semantic subtyping. In Logic in Computer Science. 137--146. Google ScholarDigital Library
- Godefroid, P., Klarlund, N., and Sen, K. 2005. DART: Directed automated random testing. In Proceedings of the Conference on Programming Language Design and Implementation. Google ScholarDigital Library
- Gomes, B., Stoutamire, D., Vaysman, B., and Klawitter, H. 1996. A language manual for Sather 1.1. http://www.icsi.berkeley.edu/~sather/Documentation/LanguageDescription/webmaker/index.html.Google Scholar
- Gosling, J., Joy, B., and Steele, G. 1996. The Java Language Specification. Addison-Wesley. Google ScholarDigital Library
- Gronski, J. and Flanagan, C. 2007. Unifying hybrid types and contracts. In Trends in Functional Programming.Google Scholar
- Gronski, J., Knowles, K., Tomb, A., Freund, S. N., and Flanagan, C. 2006. Sage: Practical hybrid checking for expressive types and specifications. In Proceedings of the Workshop on Scheme and Functional Programming. 93--104.Google Scholar
- Haines, N., Kindred, D., Morrisett, J. G., Nettles, S., and Wing, J. M. 1994. Composing first-class transactions. ACM Trans. Program. Lang. Syst. 16, 6, 1719--1736. Google ScholarDigital Library
- Henglein, F. 1994. Dynamic typing: Syntax and proof theory. Sci. Comput. Program. 22, 3, 197--230. Google ScholarDigital Library
- Herman, D., Tomb, A., and Flanagan, C. 2007. Space-Efficient gradual typing. In Trends in Functional Programming. 404--419.Google Scholar
- Holt, R. C. and Cordy, J. R. 1988. The Turing programming language. Comm. ACM 31, 1310--1424. Google ScholarDigital Library
- Knowles, K. and Flanagan, C. 2007. Type reconstruction for general refinement types. In Proceedings of the European Symposium on Programming. 505--519. Google ScholarDigital Library
- Kölling, M. and Rosenberg, J. 1997. Blue: Language specification, version 0.94.Google Scholar
- Leavens, G. T. and Cheon, Y. 2005. Design by contract with JML. http://www.cs.iastate.edu/~leavens/JML/.Google Scholar
- Luckham, D. 1990. Programming with specifications. Texts and Monographs in Computer Science. Google ScholarDigital Library
- Mandelbaum, Y., Walker, D., and Harper, R. 2003. An effective theory of type refinements. In Proceedings of the International Conference on Functional Programming. ACM Press, New York, 213--225. Google ScholarDigital Library
- Meyer, B. 1988. Object-Oriented Software Construction. Prentice Hall. Google ScholarDigital Library
- Morrisett, G., Walker, D., Crary, K., and Glew, N. 1999. From System F to typed assembly language. ACM Trans. Program. Lang. Syst. 21, 3, 527--568. Google ScholarDigital Library
- Necula, G. C. 1997. Proof-Carrying code. In Symposium on Principles of Programming Languages. Google ScholarDigital Library
- Necula, G. C., McPeak, S., and Weimer, W. 2002. CCured: Type-Safe retrofitting of legacy code. In Proceedings of the Symposium on Principles of Programming Languages. 128--139. Google ScholarDigital Library
- O'Callahan, R. and Choi, J.-D. 2003. Hybrid dynamic data race detection. In Proceedings of the Symposium on Principles and Practice of Parallel Programming. 167--178. Google ScholarDigital Library
- Ou, X., Tan, G., Mandelbaum, Y., and Walker, D. 2004. Dynamic typing with dependent types. In Proceedings of the IFIP International Conference on Theoretical Computer Science. 437--450.Google Scholar
- Rondon, P. M., Kawaguchi, M., and Jhala, R. 2008. Liquid types. In Proceeding of the Conference on Programming Language Design and Implementation. Google ScholarDigital Library
- Siek, J. and Taha, W. 2007. Gradual typing for objects. In Proceedings of the European Conference on Object Oriented Programming. 2--27. Google ScholarDigital Library
- Siek, J. G. and Taha, W. 2006. Gradual typing for functional languages. In Proceedings of the Workshop on Scheme and Functional Programming.Google Scholar
- Statman, R. 1985. Logical relations and the typed lambda-calculus. Inform. Control 65, 2-3, 85--97.Google ScholarCross Ref
- Tarditi, D., Morrisett, G., Cheng, P., Stone, C., Harper, R., and Lee, P. 1996. TIL: A type-directed optimizing compiler for ML. ACM SIGPLAN Not. 31, 5, 181--192. Google ScholarDigital Library
- Thatte, S. 1990. Quasi-Static typing. In Proceedings of the Symposium on Principles of Programming Languages. 367--381. Google ScholarDigital Library
- Vitek, J., Jagannathan, S., Welc, A., and Hosking, A. L. 2004. A semantic framework for designer transactions. In Proceedings of the European Symposium on Programming. 249--263.Google Scholar
- von Praun, C. and Gross, T. 2001. Object race detection. In Proceedings of the Conference on Object-Oriented Programming, Systems, Languages and Applications. 70--82. Google ScholarDigital Library
- Wadler, P. and Findler, R. B. 2007. Well-Typed programs can't be blamed. In Proceedings of the Workshop on Scheme and Functional Programming.Google Scholar
- Wright, A. and Cartwright, R. 1994. A practical soft type system for scheme. In Proceedings of the Conference on Lisp and Functional Programming. 250--262. Google ScholarDigital Library
- Wright, A. and Felleisen, M. 1994. A syntactic approach to type soundness. Inform. Comput. 115, 1, 38--94. Google ScholarDigital Library
- Xi, H. 2000. Imperative programming with dependent types. In Proceedings of the Annual IEEE Symposium on Logic in Computer Science (LICS'00). 375--387. Google ScholarDigital Library
- Xi, H. and Pfenning, F. 1999. Dependent types in practical programming. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (PoPL'99). ACM Press, New York, 214--227. Google ScholarDigital Library
Index Terms
- Hybrid type checking
Recommendations
Hybrid type checking
POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languagesTraditional static type systems are very effective for verifying basic interface specifications, but are somewhat limited in the kinds specifications they support. Dynamically-checked contracts can enforce more precise specifications, but these are not ...
Hybrid type checking
Proceedings of the 2006 POPL ConferenceTraditional static type systems are very effective for verifying basic interface specifications, but are somewhat limited in the kinds specifications they support. Dynamically-checked contracts can enforce more precise specifications, but these are not ...
Polymorphic Manifest Contracts, Revised and Resolved
Manifest contracts track precise program properties by refining types with predicates—for example, {x:Int∣ x > 0} denotes the positive integers. Contracts and polymorphism make a natural combination: programmers can give strong contracts to abstract ...
Reviews
Pierre Jouvelot
Many programming languages rely on static typing systems to help software engineers catch errors as soon as possible. However, having to decide type satisfiability at compile time severely constrains the design space of such systems; more sophisticated and thus useful types could be introduced if one could delay type checking to runtime. This paper introduces hybrid type systems that rely on a static typing discipline whenever possible and only revert to runtime checks when type compatibility cannot be asserted at compile time. Hybrid type systems strive to offer the best of both worlds: advanced type safety at the lowest performance cost possible. The authors illustrate hybrid type checking on a typed lambda calculus extended with type coercion expressions that perform runtime type compatibility checks. Types are based on refinement types, which denote sets of values that verify a given arbitrary Boolean predicate. Such an expressive dependent type system is undecidable, although some checking can be performed statically, depending on the power of the Boolean theorem prover used by the type checker. In this setting, type checking a lambda calculus expression not only ensures that its subexpressions are properly typed (whenever possible), but also returns a copy of the initial expression, in which some dynamic runtime type checks may have been added (when the prover fails to be conclusive). This reconstruction algorithm and its correctness proof are provided in the paper. Designers of type systems will find this easy-to-read paper a valuable contribution to the field. Online Computing Reviews Service
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments