Hybrid type checking

ABSTRACT

Traditional 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 checked until run time, 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 paper explores the key ideas and implications of hybrid type checking, in the context of the simply-typed λ-calculus with arbitrary refinements of base types.

REFERENCES

• 1: M. Abadi , L. Cardelli , B. Pierce , G. Plotkin, Dynamic typing in a statically-typed language, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.213-227, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75296]
• 2: R. Agarwal and S. D. Stoller. Type inference for parameterized race-free Java. In Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation, pages 149--160, 2004.
• 3: Alexander Aiken , Edward L. Wimmers , T. K. Lakshman, Soft typing with conditional types, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.163-173, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.177847]
• 4: Lennart Augustsson, Cayenne—a language with dependent types, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.239-250, September 26-29, 1998, Baltimore, Maryland, United States
• 5: Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.203-213, June 2001, Snowbird, Utah, United States
• 6: D. Blei, C. Harrelson, R. Jhala, R. Majumdar, G. C. Necula, S. P. Rahul, W. Weimer, and D. Weitz. Vampyre. Information available from http://www-cad.eecs.berkeley.edu/rupak/Vampyre/, 2000.
• 7: Val Breazu-Tannen , Thierry Coquand , Carl A. Gunter , Andre Scedrov, Inheritance as implicit coercion, Information and Computation, v.93 n.1, p.172-221, July 1991 [doi>10.1016/0890-5401(91)90055-7]
• 8: L. Burdy, Y. Cheon, D. Cok, M. Ernst, J. Kiniry, G. Leavens, K. Leino, and E. Poll. An overview of JML tools and applications, 2003.
• 9: L. Cardelli. Phase distinctions in type theory. Manuscript, 1988.
• 10: L. Cardelli, Typechecking dependent types and subtypes, Lecture notes in computer science on Foundations of logic and functional programming, p.45-57, June 1988, Trento, Italy
• 11: Rowan Davies , Frank Pfenning, Intersection types and computational effects, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.198-208, September 2000
• 12: David Detlefs , Greg Nelson , James B. Saxe, Simplify: a theorem prover for program checking, Journal of the ACM (JACM), v.52 n.3, p.365-473, May 2005 [doi>10.1145/1066100.1066102]
• 13: Robert Bruce Findler , Matthias Felleisen, Behavioral software contracts, 2002
• 14: Robert Bruce Findler , Matthias Felleisen, Contracts for higher-order functions, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.48-59, October 04-06, 2002, Pittsburgh, PA, USA
• 15: Cormac Flanagan , Matthew Flatt , Shriram Krishnamurthi , Stephanie Weirich , Matthias Felleisen, Catching bugs in the web of program invariants, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.23-32, May 21-24, 1996, Philadelphia, Pennsylvania, United States
• 16: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 17: Tim Freeman , Frank Pfenning, Refinement types for ML, Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation, p.268-277, June 24-28, 1991, Toronto, Ontario, Canada
• 18: Patrice Godefroid , Nils Klarlund , Koushik Sen, DART: directed automated random testing, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 19: B. Gomes, D. Stoutamire, B. Vaysman, and H. Klawitter. A language manual for Sather 1.1, 1996.
• 20: James Gosling , Bill Joy , Guy Steele , Gilad Bracha, Java(TM) Language Specification, The (3rd Edition) (Java (Addison-Wesley)), Addison-Wesley Professional, 2005
• 21: Nicholas Haines , Darrell Kindred , J. Gregory Morrisett , Scott M. Nettles , Jeannette M. Wing, Composing first-class transactions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.6, p.1719-1736, Nov. 1994 [doi>10.1145/197320.197346]
• 22: Fritz Henglein, Dynamic typing: syntax and proof theory, Science of Computer Programming, v.22 n.3, p.197-230, June 1994
• 23: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , George C. Necula , Grégoire Sutre , Westley Weimer, Temporal-Safety Proofs for Systems Code, Proceedings of the 14th International Conference on Computer Aided Verification, p.526-538, July 27-31, 2002
• 24: Richard C. Holt , James R. Cordy, The Turing programming language, Communications of the ACM, v.31 n.12, p.1410-1423, Dec. 1988 [doi>10.1145/53580.53581]
• 25: M. Kölling and J. Rosenberg. Blue: Language specification, version 0.94, 1997.
• 26: G. T. Leavens and Y. Cheon. Design by contract with JML, 2005. avaiable at http://www.cs.iastate.edu/~leavens/JML/#.
• 27: David C. Luckham, Programming with Specifications: An Introduction to Anna, a Language for Specifying ADA Programs, Springer-Verlag New York, Inc., Secaucus, NJ, 1990
• 28: M. Fagan. Soft Typing. PhD thesis, Rice University, 1990.
• 29: Yitzhak Mandelbaum , David Walker , Robert Harper, An effective theory of type refinements, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, p.213-225, August 25-29, 2003, Uppsala, Sweden
• 30: Bertrand Meyer, Object-Oriented Software Construction, Prentice-Hall, Inc., Upper Saddle River, NJ, 1988
• 31: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.3, p.527-568, May 1999 [doi>10.1145/319301.319345]
• 32: George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
• 33: George C. Necula , Scott McPeak , Westley Weimer, CCured: type-safe retrofitting of legacy code, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.128-139, January 16-18, 2002, Portland, Oregon
• 34: Robert O'Callahan , Jong-Deok Choi, Hybrid dynamic data race detection, Proceedings of the ninth ACM SIGPLAN symposium on Principles and practice of parallel programming, June 11-13, 2003, San Diego, California, USA
• 35: X. Ou, G. Tan, Y. Mandelbaum, and D. Walker. Dynamic typing with dependent types. In IFIP International Conference on Theoretical Computer Science, pages 437--450, 2004.
• 36: D. L. Parnas, A technique for software module specification with examples, Communications of the ACM, v.15 n.5, p.330-336, May 1972 [doi>10.1145/355602.361309]
• 37: John C. Reynolds, Definitional interpreters for higher-order programming languages, Proceedings of the ACM annual conference, p.717-740, August 01-01, 1972, Boston, Massachusetts, United States [doi>10.1145/800194.805852]
• 38: Satish Thatte, Quasi-static typing, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.367-381, December 1989, San Francisco, California, United States [doi>10.1145/96709.96747]
• 39: D. Tarditi , G. Morrisett , P. Cheng , C. Stone , R. Harper , P. Lee, TIL: a type-directed optimizing compiler for ML, ACM SIGPLAN Notices, v.31 n.5, p.181-192, May 1996
• 40: J. Vitek, S. Jagannathan, A. Welc, and A. L. Hosking. A semantic framework for designer transactions. In Proceedings of European Symposium on Programming, pages 249--263, 2004.
• 41: Christoph von Praun , Thomas R. Gross, Object race detection, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.70-82, October 14-18, 2001, Tampa Bay, FL, USA
• 42: Andrew K. Wright , Robert Cartwright, A practical soft type system for Scheme, Proceedings of the 1994 ACM conference on LISP and functional programming, p.250-262, June 27-29, 1994, Orlando, Florida, United States
• 43: Andrew K. Wright , Matthias Felleisen, A syntactic approach to type soundness, Information and Computation, v.115 n.1, p.38-94, Nov. 15, 1994 [doi>10.1006/inco.1994.1093]
• 44: Hongwei Xi, Imperative Programming with Dependent Types, Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, p.375, June 26-29, 2000
• 45: Hongwei Xi , Frank Pfenning, Dependent types in practical programming, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.214-227, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292560]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

General Terms:
Languages, Theory, Verification

Keywords:
contracts, dynamic checking, static checking, type systems