Static typing for a substructural lambda calculus

Abstract

Substructural type systems are designed from the insight inspired by the development of linear and substructural logics. Substructural type systems promise to control the usage of computational resources statically, thus detect more program errors at an early stage than traditional type systems do. In the past decade, substructural type systems have been deployed in the design of novel programming languages, such as Vault, etc. This paper presents a general typing theory for substructural type system. First, we define a universal semantic framework for substructural types by interpreting them as characteristic intervals composed of type qualifiers. Based on this framework, we present the design of a substructural calculus λ_SL with subtyping relations. After giving syntax, typing rules and operational semantics for λ_SL, we prove the type safety theorem. The new calculus λ_SL can guarantee many more safety invariants than traditional lambda calculus, which is demonstrated by showing that the λ_SL calculus can serve as an idealized type intermediate language, and defining a type- preserving translation from ordinary typed lambda calculus into λ_SL.

Keywords

Programming languages / linear type systems / substructural type system / subtyping theory / type preserving translation

References

[1] Girard J Y. Linear logic. Theoretical Computer Science, 1987, 50: 1-102

[2] Girard J Y. On the uinty of logic. Annals of Pure and Applied Logic, 1993, 59(3): 201-217

[3] Wadler P. Linear types can change the world! In: Proceedings of IFIP TC 2 Working Conference on Programming Concepts and Methods. 1990, 347-359

[4] Wadler P. Is there a use for linear logic? In: Proceedings of the 1991 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation. 1991, 255-273

[5] Walker D, Watkins K. On regions and linear types (extended abstract). In: Proceedings of the 6th ACM SIGPLAN international conference on Functional Programming. 2001, 181-192

[6] Wansbrough K, Jones S P. Once upon a polymorphic type. In: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages. 1999, 15-28

[7] Kobayashi N. Quasi-linear types. In: Proceedings of the 26th ACM SIGPLAN-SIGACT on Principles of Programming Languages. 1999, 29-42

[8] Polakow J. Linear logic programming with an ordered context. In: Proceedings of the 2nd ACM SIGPLAN Conference on Principles and Practice of Declarative Programming. 2000, 68-79.

[9] Polakow J, Pfenning F. Ordered linear logic programming. Technical Report CMU-CS-98–183, Department of Computer Science, Carnegie Mellon University, <month>December</month>1998.

[10] Smith F, Walker D, Morrisett J G. Alias types. In: Proceedings of 9th European Symposium on Programming. 2000, 366-381

[11] Mandelbaum Y, Walker D, Harper R. An effective theory of type refinements. In: Proceedings of Proc. of the 8th ACM SIGPLAN International Conference on Functional Programming. 2003, 213-226

[12] Walker D. Substructural type systems. In: Pierce B C, eds, Advanced Topics in Types and Programming Languages. Cambridge: MIT Press, 2005

[13] Kernighan B W, Ritchie D M. The C programming Language. Upper Saddle River: Prentice-Hall, 1988

[14] Foster J S, Fähndrich M, Aiken A. A theory of type qualifiers. In: Proceedings of the 1999 ACM SIGPLAN Conference on Programming Language Design and Implementation. 1999, 192-203

[15] Foster J S, Terauchi T, Aiken A. Flow-Sensitive Type Qualifiers. In: Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation. 2002, 1-12

[16] Polakow J. Ordered linear logic and applications. Dissertation for the Doctoral Degree. Pittsburgh: Carnegie Mellon University, 2001

RIGHTS & PERMISSIONS

2014 Higher Education Press and Springer-Verlag Berlin Heidelberg