Languages of the future

ABSTRACT

This paper explores a new point in the design space of formal reasoning systems - part programming language, part logical framework. The system is built on a programming language where the user expresses equality constraints between types and the type checker then enforces these constraints. This simple extension to the type system allows the programmer to describe properties of his program in the types of witness objects which can be thought of as concrete evidence that the program has the property desired. These techniques and two other rich typing mechanisms, rank-N polymorphism and extensible kinds, create a powerful new programming idiom for writing programs whose types enforce semantic properties. This kind of synthesis between a practical programming language <i>and</i> a logic creates a foundation for the design of languages of the future.

REFERENCES

• 1: P. Bertelsen. Semantics of Java Byte Code. Technical report, Dep. of Information Technology, Technical University of Denmark, March 1997.
• 2: Frédéric Besson , Thomas de Grenier de Latour , Thomas Jensen, Secure calling contexts for stack inspection, Proceedings of the 4th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.76-87, October 06-08, 2002, Pittsburgh, PA, USA [doi>10.1145/571157.571166]
• 3: C. Calcagno , E. Moggi , T. Sheard, Closed types for a safe imperative MetaML, Journal of Functional Programming, v.13 n.3, p.545-571, May 2003 [doi>10.1017/S0956796802004598]
• 4: Chiyan Chen , Hongwei Xi, Meta-programming through typeful code representation, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, p.275-286, August 25-29, 2003, Uppsala, Sweden
• 5: James Cheney and Ralf Hinze. Phantom types. Available from http://www.informatik.uni-bonn.de ralf/publications/Phantom.pdf|.,2003.
• 6: Karl Crary , Stephnie Weirich, Resource bound certification, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.184-198, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325716]
• 7: Simon Peyton Jones and Mark Shields. Practical type inference for arbitrary-rank types. Technical report, Microsoft Research, "December" 2003. http://research.microsoft.com/Users/simonpj/papers/putting/index.htm.
• 8: John Launchbury , Ross Paterson, Parametricity and Unboxing with Unpointed Types, Proceedings of the 6th European Symposium on Programming Languages and Systems, p.204-218, April 22-24, 1996
• 9: Didier Le Botlan , Didier Rémy, ML^F: raising ML to the power of system F, ACM SIGPLAN Notices, v.38 n.9, p.27-38, September 2003
• 10: 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]
• 11: Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. TALx86: A realistic typed assembly language. ACM SIGPLAN Workshop on Compiler Support for System Software, 1999.
• 12: P. Ørbæk , J. Palsberg, Trust in the λ-calculus, Journal of Functional Programming, v.7 n.6, p.557-591, November 1997 [doi>10.1017/S0956796897002906]
• 13: Lawrence C. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science, pages 361--386. Academic Press, 1990.
• 14: Frank Pfenning , Carsten Schürmann, System Description: Twelf - A Meta-Logical Framework for Deductive Systems, Proceedings of the 16th International Conference on Automated Deduction: Automated Deduction, p.202-206, July 07-10, 1999
• 15: Andrei Sabelfeld and Andrew C. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1):5--19, January 2003.
• 16: Tim Sheard , Simon Peyton Jones, Template meta-programming for Haskell, Proceedings of the 2002 ACM SIGPLAN workshop on Haskell, p.1-16, October 03, 2002, Pittsburgh, Pennsylvania [doi>10.1145/581690.581691]
• 17: Vincent Simonet, An extension of HM(X) with bounded existential and universal data-types, ACM SIGPLAN Notices, v.38 n.9, p.39-50, September 2003
• 18: Raymie Stata , Martín Abadi, A type system for Java bytecode subroutines, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.149-160, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268959]
• 19: Walid Taha, A sound reduction semantics for untyped CBN mutli-stage computation. Or, the theory of MetaML is non-trival (extended abstract), Proceedings of the 2000 ACM SIGPLAN workshop on Partial evaluation and semantics-based program manipulation, p.34-43, January 22-23, 2000, Boston, Massachusetts, United States
• 20: Walid Taha , Tim Sheard, MetaML and multi-stage programming with explicit annotations, Theoretical Computer Science, v.248 n.1-2, p.211-242, October 2000 [doi>10.1016/S0304-3975(00)00053-0 ]
• 21: The Coq Development Team. The Coq Proof Assistant Reference Manual, Version 7.4. INRIA, 2003. http://pauillac.inria.fr/coq/doc/main.html.
• 22: Joseph C. Vanderwaart and Karl Crary. Foundational typed assembly language for grid computing. Technical Report CMU-CS-04-104, Carnegie Mellon University, 2004.
• 23: Dennis Volpano , Cynthia Irvine , Geoffrey Smith, A sound type system for secure flow analysis, Journal of Computer Security, v.4 n.2-3, p.167-187, Jan. 1996
• 24: Philip Wadler, Comprehending monads, Proceedings of the 1990 ACM conference on LISP and functional programming, p.61-78, June 27-29, 1990, Nice, France [doi>10.1145/91556.91592]
• 25: Philip Wadler, The essence of functional programming, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-14, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143169]
• 26: Philip Wadler. Monads for functional programming. In M. Broy, editor, Program Design Calculi, volume 118 of NATO ASI series, Series F: Computer and System Sciences. Springer Verlag, 1994. Proceedings of the International Summer School at Marktoberdorf directed by F. L. Bauer, M. Broy, E. W. Dijkstra, D. Gries, and C. A. R. Hoare.
• 27: D. S. Wallach and E. W. Felten. Understanding java stack inspection. In 1998 IEEE Symposium on Security and Privacy (SSP '98), pages 52--65, Washington - Brussels - Tokyo, May 1998. IEEE.
• 28: Hongwei Xi , Frank Pfenning, Eliminating array bound checking through dependent types, ACM SIGPLAN Notices, v.33 n.5, p.249-257, May 1998
• 29: 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

General Terms:
Design, Languages, Theory, Verification

Keywords:
equality constrained types, formal methods, formal reasoning systems, staged languages, static constraint management