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 ScholarDigital 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 ...
Comments